diff --git a/dag/gunbc/guarantee_rung_drop.dag b/dag/gunbc/guarantee_rung_drop.dag index ba27371a64c..49e377fbcc4 100644 --- a/dag/gunbc/guarantee_rung_drop.dag +++ b/dag/gunbc/guarantee_rung_drop.dag @@ -544,3 +544,54 @@ fn stall_roster_size(ss: List) -> Int { cons: fn(acc, s) { acc + 1 }, ) } + +// THE CONNECTIVE GAP, DECLARED RATHER THAN CLAIMED (DESIGN section 4b(2): a class below its ceiling +// names its next-rung trigger). Ordering and arithmetic on a structural operand are decided by this +// roster -- a declared comparison, or a typed refusal. The logical connectives are NOT: inference +// constrains only the RESULT of `&&`/`||` to Bool (v1.compiler.types infer_binop_type_node), so a +// structural operand under a connective is authorable and renders as the host token. Found by +// review (claude/claude-opus-4-7 on gunbc#9719, 2026-08-30) reading the arm against its own prose. +// +// WHY THE OBVIOUS REPAIR IS THE WRONG ONE, measured before it was rejected: refusing every +// structural operand under a connective would refuse v2.std.logic Bool, which 593 modules import as +// their ordinary Bool -- the false-refusal cost the namespace wall's own doctrine names, and it +// would land as a corpus-wide red rather than as a wall. The repair is one more row FAMILY of the +// shape this roster already carries for ordering: the declaration names the operation that realizes +// its conjunction and disjunction, connectives on a declaration with a row realize through it, and +// only a declaration with NO row refuses -- at which point the refusal population is enumerable +// instead of being the whole corpus. +// TWO Nat AUTHORITIES ARE ONE NAME ANSWERING FOR TWO CONCEPTS, and this row exists because review +// 57758 correctly refused a version of it that was narrated in prose beside one of the two nat_max +// declarations. The fork predates this lane; what this lane changed is that the Peano side now +// carries real operations, so the fork is load-bearing rather than latent. +data two_nat_authorities_stall: GuaranteeStall = GuaranteeStall { + subject: "std.nat Nat (CommutativeSemiring, realizing natively as a machine scalar) and v2.std.nat Nat (the Peano coproduct Zero | Succ) are two declarations answering for one name, so nat_add / nat_mul / nat_max / nat_compare each exist twice and a bare reference in a closure containing both modules is ambiguous", + current: Mitigatable, + ceiling: StructurallyImpossible, + blocker: AwaitsOneGrounding { + grounding: "one Nat authority: the numeric tower deciding whether the Peano coproduct IS the declaration and the semiring alias is derived from it, or the reverse -- a modeling ruling this lane cannot make from an operator-realization change", + }, + population: BoundedPopulation { + members: [ + "std.nat and v2.std.nat both declaring Nat, with per-operation forks (nat_add, nat_mul, nat_max, nat_compare) that no single function can serve because the two are different types", + "every reference site in a closure containing both modules, which must qualify the name (v2.lens.cost.valuation does) or resolve by pool precedence", + ], + }, + next_rung_trigger: "one Nat declaration in the corpus, with the other side derived from it rather than declared beside it -- retired by that capability and by nothing less, since deleting either declaration without deriving its operations would remove the operations its consumers call rather than unify the authority" +} + +data structural_connective_stall: GuaranteeStall = GuaranteeStall { + subject: "std.operator_realization -- a logical connective (&&, ||) applied to a STRUCTURAL operand renders as the host token, because no declared-connective row family exists to realize or refuse it", + current: Mitigatable, + ceiling: MechanicallyPreventable, + blocker: AwaitsOneGrounding { + grounding: "a StructuralConnectiveBinding row family in std.operator_realization keyed on the operand's exact DeclarationRef (the shape StructuralOrderingBinding already has), plus its rows for the declarations this corpus uses under a connective -- v2.std.logic Bool first", + }, + population: BoundedPopulation { + members: [ + "a connective whose operand is a structural declaration with no host realization (v2.std.logic Bool: renders as the host token today and is the corpus's ordinary conjunction)", + "a connective whose operand is a structural declaration that is not a Boolean algebra at all (a Peano-shaped operand: authorable because inference constrains only the result type)", + ], + }, + next_rung_trigger: "std.operator_realization declaring StructuralConnectiveBinding and operator_realization_for routing And/Or through it -- realizing where a row exists and refusing, typed and located, where none does; retired by that capability and by nothing less, since a roster with no consumer would leave the host token exactly where it is today" +} diff --git a/dag/gunbc/stage0/stage0_crate_partition_generated.dag b/dag/gunbc/stage0/stage0_crate_partition_generated.dag index 2e41077f14e..c5a1191a37b 100644 --- a/dag/gunbc/stage0/stage0_crate_partition_generated.dag +++ b/dag/gunbc/stage0/stage0_crate_partition_generated.dag @@ -71,6 +71,8 @@ data generated_partition_crate_rows: List = [ "std_occurrence_identity", "std_source_annotation", "std_target_representation", + "std_literal_elaboration", + "std_operator_realization", "v1_std_core" ], reexport_packages: [ @@ -147,6 +149,7 @@ data generated_partition_crate_rows: List = [ kind: GeneratedLayeredCoreCrate, modules: [ "gunbc_rust_source_type_bindings", + "gunbc_structural_realization_bindings", "v1_compiler_coercion", "v1_compiler_infer_emit_info", "v1_compiler_infer_env", diff --git a/dag/gunbc/structural_realization_bindings.dag b/dag/gunbc/structural_realization_bindings.dag new file mode 100644 index 00000000000..bb28e10cf8c --- /dev/null +++ b/dag/gunbc/structural_realization_bindings.dag @@ -0,0 +1,64 @@ +module gunbc.structural_realization_bindings + +import std.types { List, String, Bool, NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import std.literal_elaboration { LiteralHomomorphism, LiteralSourceKind, KernelIntLiteral, KernelBoolLiteral, LiteralUnfolding, PeanoUnfold, BooleanUnfold } +import std.operator_realization { StructuralOrderingBinding } + +// THE CORPUS'S HALF OF LITERAL ELABORATION AND OPERATOR REALIZATION (std.literal_elaboration, +// std.operator_realization): which of THIS corpus's structural declarations supply a kernel literal, +// and through which of their own constructors; and which declare an ordering, and by which +// comparison. Keyed on the exact declaration, never on a spelling: std.nat Nat (a native-realizing +// semiring alias) and v2.std.nat Nat (the Peano coproduct) share a spelling and only the second is +// a row here. The sibling gunbc.rust_source_type_bindings answers the OTHER question -- which +// declarations realize natively on the Rust target -- and a declaration is never in both: a native +// realization takes the kernel literal directly and the host operator directly. +// +// A ROW MAY ONLY STATE A HOMOMORPHISM THAT IS ALREADY TRUE OF THE DESTINATION, never be added to +// make a failing site compile (the same discipline gunbc.rust_source_type_bindings and +// v1.compiler.coercion numeric_realization_roster_extension_note hold for the native roster). The +// Peano row is true by the definition of the naturals: n maps to succ^n(zero), and that map is the +// unique semiring homomorphism from the kernel integers restricted to the nonnegatives. + +fn peano_literal_homomorphism(module_path: String, nat: String, zero: String, succ: String, prev_field: String) -> LiteralHomomorphism { + LiteralHomomorphism { + source_kind: KernelIntLiteral, + destination: decl_ref(module_path: module_path, decl_name: nat), + producer: PeanoUnfold { + zero: decl_ref(module_path: module_path, decl_name: zero), + succ: decl_ref(module_path: module_path, decl_name: succ), + prev_field: prev_field as NonEmptyStr + } + } +} + +fn boolean_literal_homomorphism(module_path: String, bool_decl: String, true_variant: String, false_variant: String) -> LiteralHomomorphism { + LiteralHomomorphism { + source_kind: KernelBoolLiteral, + destination: decl_ref(module_path: module_path, decl_name: bool_decl), + producer: BooleanUnfold { + true_variant: decl_ref(module_path: module_path, decl_name: true_variant), + false_variant: decl_ref(module_path: module_path, decl_name: false_variant) + } + } +} + +// v2.std.logic Bool = True | False is gated structural on purpose (v1.compiler.coercion +// structural_declaration_modules_for); the corpus-wide prelude std.types Bool realizes natively and +// is NOT a row -- a kernel true/false at that boundary stays the host bool. +data literal_homomorphism_rows: List = [ + peano_literal_homomorphism(module_path: "v2.std.nat", nat: "Nat", zero: "Zero", succ: "Succ", prev_field: "prev"), + boolean_literal_homomorphism(module_path: "v2.std.logic", bool_decl: "Bool", true_variant: "True", false_variant: "False") +] + +fn structural_ordering_binding(carrier_module: String, carrier: String, compare_module: String, compare: String, ordering_module: String, ordering: String) -> StructuralOrderingBinding { + StructuralOrderingBinding { + carrier: decl_ref(module_path: carrier_module, decl_name: carrier), + compare: decl_ref(module_path: compare_module, decl_name: compare), + ordering: decl_ref(module_path: ordering_module, decl_name: ordering) + } +} + +data structural_ordering_rows: List = [ + structural_ordering_binding(carrier_module: "v2.std.nat", carrier: "Nat", compare_module: "v2.std.nat", compare: "nat_compare", ordering_module: "std.algebra", ordering: "Ordering") +] diff --git a/dag/std/literal_elaboration.dag b/dag/std/literal_elaboration.dag new file mode 100644 index 00000000000..a273c88fdfc --- /dev/null +++ b/dag/std/literal_elaboration.dag @@ -0,0 +1,167 @@ +module std.literal_elaboration + +import std.types { List, String, Bool, Int, NonEmptyStr } +import std.decl_ref { DeclarationRef, declaration_ref_eq } +import std.syntax { LiteralValue, LitStr, LitInt, LitFloat, LitBool, LitNull, LitSymbol } + +// THE EXPECTED-TYPE-DIRECTED LITERAL INTRODUCTION JUDGMENT, as a model (DESIGN section 4: one +// decision procedure, emission and ingestion are the same homomorphism check read in two directions). +// +// A kernel literal (`0`, `"x"`, `true`, `^s`) is a value of the KERNEL type the parser mints for it. +// When such a literal reaches a typed boundary -- a call argument, a declared return, a record +// field, a data initializer, an annotated let, the other operand of a binary operator -- the +// boundary names a DESTINATION declaration. Three things can be true of that pair, and they are +// three outcomes, never one row with a flag: +// DirectLiteral the destination realizes the kernel type itself (a host numeric, the kernel +// type, a native-realizing alias): the literal is already its own value. +// ViaHomomorphism the destination is a STRUCTURAL declaration that SUPPLIES the literal: one +// declared homomorphism from the kernel value into the destination's own +// constructors (a Peano numeral into Zero/Succ, a text into a FreeMonoid of +// scalars). The typed tree carries the destination and the homomorphism at the +// occurrence; emission renders the image and never re-decides from spelling. +// Refused the roster is defective at this key (two rows for one destination). +// A destination with NO row and no native realization is not refused HERE: whether a kernel +// numeral inhabits such a declaration is the inhabitance judgment's question and it already owns +// that refusal (v1.compiler.infer declared_type_inhabitance). Answering it twice would be the two- +// authority state DESIGN section 3 forbids; this judgment introduces values, it does not police them. +// +// GENERIC BY CONSTRUCTION. The judgment is keyed on (source kind, exact destination DeclarationRef) +// and the image is produced by a closed roster of UNFOLDINGS, one arm per structural shape a kernel +// value can be unfolded into. A consumer that needs a new destination adds one ROW to the corpus +// roster (gunbc.structural_realization_bindings) and, if its destination's shape is new, one +// unfolding ARM here -- never a second elaboration fold and never a per-destination special case +// in inference or emission. The Peano arm is the first inhabitant; the FreeMonoid-of-scalars arm +// is the structural-text lane's (XL-0T) to add beside it. +// +// WHY A NEGATIVE-VALUE REFUSAL IS ABSENT ON PURPOSE (DESIGN section 4b: ask whether the RED is +// authorable before writing the check). A kernel integer literal is never negative -- `-3` parses +// as a unary negation applied to the literal `3`, and the negation is an ordinary expression that +// reaches inference through its own arm, not through this judgment. A ValueOutsideHomomorphismDomain +// arm for the Peano unfolding would therefore be permanently green and would be cited as coverage. + +type LiteralSourceKind + = KernelIntLiteral + | KernelStringLiteral + | KernelFloatLiteral + | KernelBoolLiteral + | KernelSymbolLiteral + | KernelNullLiteral + +fn literal_source_kind_of(value: LiteralValue) -> LiteralSourceKind { + match value { + LitInt { value: _ } => KernelIntLiteral + LitStr { value: _ } => KernelStringLiteral + LitFloat { value: _ } => KernelFloatLiteral + LitBool { value: _ } => KernelBoolLiteral + LitSymbol { value: _ } => KernelSymbolLiteral + LitNull => KernelNullLiteral + } +} + +fn literal_source_kind_label(kind: LiteralSourceKind) -> String { + match kind { + KernelIntLiteral => "kernel_int_literal" + KernelStringLiteral => "kernel_string_literal" + KernelFloatLiteral => "kernel_float_literal" + KernelBoolLiteral => "kernel_bool_literal" + KernelSymbolLiteral => "kernel_symbol_literal" + KernelNullLiteral => "kernel_null_literal" + } +} + +fn literal_source_kind_eq(a: LiteralSourceKind, b: LiteralSourceKind) -> Bool { + literal_source_kind_label(kind: a) == literal_source_kind_label(kind: b) +} + +// HOW A KERNEL VALUE IS UNFOLDED INTO A DESTINATION'S CONSTRUCTORS. Each arm names the destination's +// own constructors by exact DeclarationRef -- the unfolding is a fact about the destination, so a +// renamed variant is a changed row, never a stale spelling inside the compiler. +// PeanoUnfold a nonnegative integer n unfolds to succ^n(zero): `succ { prev_field: ... }` nested +// n deep around the nullary `zero`. +// BooleanUnfold a kernel bool unfolds to the destination's nullary true or false constructor +// (v2.std.logic Bool = True | False, declared structural on purpose). +type LiteralUnfolding + = PeanoUnfold { zero: DeclarationRef, succ: DeclarationRef, prev_field: NonEmptyStr } + | BooleanUnfold { true_variant: DeclarationRef, false_variant: DeclarationRef } + +type LiteralHomomorphism { + source_kind: LiteralSourceKind + destination: DeclarationRef + producer: LiteralUnfolding +} + +type LiteralHomomorphismLookup + = LiteralHomomorphismFound { row: LiteralHomomorphism } + | LiteralHomomorphismAbsent + | LiteralHomomorphismAmbiguous { row_count: Int } + +fn literal_homomorphism_for( + rows: List, + source_kind: LiteralSourceKind, + destination: DeclarationRef +) -> LiteralHomomorphismLookup { + let matching = rows |> filter(r => + literal_source_kind_eq(a: r.source_kind, b: source_kind) + && declaration_ref_eq(a: r.destination, b: destination)) + let n = matching |> count + if n == 0 { + LiteralHomomorphismAbsent + } else if n == 1 { + match matching |> first { + Present { value: row } => LiteralHomomorphismFound { row: row } + Absent => LiteralHomomorphismAbsent + } + } else { + LiteralHomomorphismAmbiguous { row_count: n } + } +} + +type LiteralElaborationRefusal + = HomomorphismDuplicated { source_kind: LiteralSourceKind, destination: DeclarationRef, row_count: Int } + +fn literal_elaboration_refusal_message(cause: LiteralElaborationRefusal) -> String { + match cause { + HomomorphismDuplicated { source_kind: k, destination: d, row_count: n } => + concat( + "literal elaboration: ", literal_source_kind_label(kind: k), " into ", + d.module_path as String, ".", d.decl_name as String, + " has more than one declared homomorphism (gunbc.structural_realization_bindings authoring defect)" + ) + } +} + +// THE DECISION. `destination_realizes_natively` is the caller's answer to "does this declaration +// realize the kernel type itself" (v1.compiler.coercion decl_file_realizes_natively / the exact +// Rust binding), passed in rather than re-derived so this module stays target-agnostic. +type LiteralElaborationOutcome + = DirectLiteral + | ViaHomomorphism { homomorphism: LiteralHomomorphism } + | LiteralElaborationRefused { cause: LiteralElaborationRefusal } + +fn elaborate_literal_at( + rows: List, + source_kind: LiteralSourceKind, + destination: DeclarationRef, + destination_realizes_natively: Bool +) -> LiteralElaborationOutcome { + if destination_realizes_natively { + DirectLiteral + } else { + match literal_homomorphism_for(rows: rows, source_kind: source_kind, destination: destination) { + LiteralHomomorphismFound { row: row } => ViaHomomorphism { homomorphism: row } + LiteralHomomorphismAbsent => DirectLiteral + LiteralHomomorphismAmbiguous { row_count: n } => + LiteralElaborationRefused { cause: HomomorphismDuplicated { source_kind: source_kind, destination: destination, row_count: n } } + } + } +} + +// WHAT THE TYPED TREE CARRIES at an elaborated occurrence: the source kind, the exact destination, +// and the homomorphism selected. The occurrence itself is the node this record sits on (its +// occurrence identity), so it is not duplicated here. Only ViaHomomorphism occurrences carry a +// record -- a DirectLiteral is the ordinary literal node and needs nothing said about it. +type LiteralElaboration { + source_kind: LiteralSourceKind + destination: DeclarationRef + homomorphism: LiteralHomomorphism +} diff --git a/dag/std/operator_realization.dag b/dag/std/operator_realization.dag new file mode 100644 index 00000000000..1b4811b0f6b --- /dev/null +++ b/dag/std/operator_realization.dag @@ -0,0 +1,292 @@ +module std.operator_realization + +import std.types { List, String, Bool, Int, NonEmptyStr } +import std.decl_ref { DeclarationRef, declaration_ref_eq } +import std.syntax { BinOp, Add, Sub, Mul, Div, Mod, Eq, Ne, Lt, Gt, Le, Ge, And, Or, NullCoalesce } + +// OPERATOR REALIZATION BY EXACT OPERAND STRUCTURE (DESIGN section 4b, the floor: an operator is +// admitted by algebra inhabitance, but what it RENDERS AS is a fact about the operand's declaration +// and the target, never about the operator's spelling). +// +// The seed emitter rendered every binary operator as the host operator token. That is correct +// exactly when the operand realizes as a host value with that operator -- a machine integer, a +// float, a bool -- and wrong for every structural declaration: a Peano coproduct has no host `<`, +// and rustc's E0369 on `Rc < Rc` was the emitter re-deciding, from the operator's +// spelling alone, a question the operand's declaration already answers. The decision is keyed on +// the operand's exact DeclarationRef and has four outcomes: +// HostOperator the operand realizes natively on the target; the host token is the op. +// StructuralEquality equality on a structural declaration: derived structurally (the target's +// structural equality over the declaration's own constructors). +// StructuralComparison an ordering on a structural declaration: a call to the declaration's +// DECLARED comparison, whose result is tested against std.algebra Ordering. +// Refused a host-only operator (arithmetic) on a structural operand that declares +// no operation for it, or an operand whose identity is unknown at the site. +// Typed and located: the line stops (DESIGN section 5), it does not emit a +// token rustc will refuse later under a code nobody joins back to the site. +// +// Arithmetic on a structural declaration is deliberately NOT realized by this decision. A Peano +// quotient with a typed zero-divisor outcome is a DECLARED OPERATION the source calls by name +// (v2.std.nat nat_div_rem); an infix `/` that silently became that call would hide the outcome the +// operation exists to expose. So the source spells structural arithmetic as calls, and this +// decision refuses the infix form on structural operands. + +// THE OPERAND'S DECLARATION AS READ AT INFERENCE, carried on the typed tree (the ExprBinOp node) +// so emission consumes it and never re-reads identity with a weaker env. Inference reads a +// parameter's type reference in the function's own scope, where the reference's ident binding is +// live; the emitter's scope is the module env, where that binding is gone and a by-name read can +// only answer the module-visible homonym (measured: `a < b` with a: v2.std.nat.Nat emitted the host +// `<` because the emitter read std.nat.Nat, which realizes natively). decl_file is the declaration's +// own file -- the key v1.compiler.coercion's native-realization decision is made on. +type OperandDeclaration { + declaration: DeclarationRef + decl_file: String +} + +type OperandRealization + = HostNumericOperand + | HostRealizedOperand { reason: HostRealizationReason } + | StructuralOperand { declaration: DeclarationRef } + | OperandIdentityUnavailable { facts: OperandShapeFacts } + +// AN OPERAND THAT REALIZES AS A HOST VALUE BY CONSTRUCTION, without a declaration to ask: the type +// the parser mints for a kernel literal or a builtin's result (a `` file, not a +// declaration in the corpus), a generic type parameter (the host bound carries the operator), a +// host container (Vec/HashMap realize the container and its comparisons), and a type node inference +// SYNTHESIZED with no authored name at all. Each is a decidable arm, named so that "no identity" +// never stands in for "host by construction". +// +// THE UNNAMED ARM IS A DISCRIMINATOR, NOT A CATCH-ALL, and it was measured before it was written. +// A structural declaration is reached by a NAME -- that is what a declaration reference is -- so a +// resolved type node whose authored name is empty is not a reference to one; it is a node inference +// built for a field access or a match-arm binder over a generic coproduct (measured: v2.compiler.02_parse +// parse_current_position, `t.start + 1` where t binds the value of ListHeadResult, is the whole +// unnamed-operand population of the v2 closure under an arithmetic operator). Refusing there would +// refuse an operand nothing suggests is structural. What still refuses is the case the refusal is +// FOR: a type node that DOES name a declaration whose identity the caller could not resolve. +type HostRealizationReason + = KernelMintedType + | GenericTypeParameter + | HostContainer + | UnnamedSynthesizedType + +// AN OPERAND WITHOUT A READABLE DECLARATION decides BY OPERATOR CLASS, never by guessing a +// declaration. Equality and the connectives do not depend on the declaration at all: every +// structural declaration realizes equality structurally and every host value realizes it natively, +// and on the target these are one token (the emitted enum derives PartialEq), so `==`/`!=`/`&&`/ +// `||`/`??` on such an operand are the host token by construction -- the same bytes a known +// declaration would produce. Ordering and arithmetic DO depend on the declaration (a declared +// comparison, or a refusal), so on an unreadable declaration they refuse, carrying the facts below. +// Measured on the v1 closure (XL-0N regen18, 50 sites / 139 refusals): every unreadable-declaration +// operand in the seed is under `==` or `!=` -- field-access and method-return type nodes inference +// synthesizes without a span -- and none is under an ordering or arithmetic operator. +// +// WHAT THE CALLER SAW when it could not read the operand's declaration -- carried on the refusal so +// a miss returns the shape, not a token rustc refuses later under E0369 (DESIGN section 5: a failure +// arm refuses, never widens; the seed's host-token fallback here was the absorbing arm that hid this +// lane's own defect behind an ordinary-looking `<`). +type OperandShapeFacts { + authored_name: String + connective: String + child_count: Int + resolved: Bool + decl_file: String +} + +// A structural declaration's declared ordering: the comparison to call and the Ordering declaration +// whose variants its result is tested against. Keyed on the carrier's exact DeclarationRef. +type StructuralOrderingBinding { + carrier: DeclarationRef + compare: DeclarationRef + ordering: DeclarationRef +} + +type StructuralOrderingLookup + = StructuralOrderingFound { row: StructuralOrderingBinding } + | StructuralOrderingAbsent + | StructuralOrderingAmbiguous { row_count: Int } + +fn structural_ordering_for(rows: List, carrier: DeclarationRef) -> StructuralOrderingLookup { + let matching = rows |> filter(r => declaration_ref_eq(a: r.carrier, b: carrier)) + let n = matching |> count + if n == 0 { + StructuralOrderingAbsent + } else if n == 1 { + match matching |> first { + Present { value: row } => StructuralOrderingFound { row: row } + Absent => StructuralOrderingAbsent + } + } else { + StructuralOrderingAmbiguous { row_count: n } + } +} + +// The test an ordering operator performs on a comparison's result, grounded on std.algebra +// Ordering = Less | Equal | Greater: `<` is `== Less`, `>` is `== Greater`, `<=` is `!= Greater`, +// `>=` is `!= Less`. Non-ordering operators have no test. +type OrderingTest + = OrderingIs { variant: NonEmptyStr } + | OrderingIsNot { variant: NonEmptyStr } + +fn ordering_test_for(op: BinOp) -> OrderingTest? { + match op { + Lt => Present { value: OrderingIs { variant: "Less" as NonEmptyStr } } + Gt => Present { value: OrderingIs { variant: "Greater" as NonEmptyStr } } + Le => Present { value: OrderingIsNot { variant: "Greater" as NonEmptyStr } } + Ge => Present { value: OrderingIsNot { variant: "Less" as NonEmptyStr } } + Add => none + Sub => none + Mul => none + Div => none + Mod => none + Eq => none + Ne => none + And => none + Or => none + NullCoalesce => none + } +} + +// THE ONLY GLYPH TABLE, AND IT IS A RENDERING FACT. The refusal carriers above hold the BinOp +// coproduct itself, never a spelling, so nothing downstream can compare operators by string. A +// spelling is required exactly once -- at the human-readable message boundary -- which is where +// this table sits. Corpus check before minting it (review 57758 asked whether the parser or the +// emitter already owns one): no BinOp-to-glyph producer exists anywhere in the tree; v1's +// compile.dag renders the VARIANT NAME ("Add"), and glyph recognition happens in the tokenizer +// against token kinds, not against a .dag row. So this is the first authority for the mapping, not +// a second one. +fn binop_label(op: BinOp) -> String { + match op { + Add => "+" + Sub => "-" + Mul => "*" + Div => "/" + Mod => "%" + Eq => "==" + Ne => "!=" + Lt => "<" + Gt => ">" + Le => "<=" + Ge => ">=" + And => "&&" + Or => "||" + NullCoalesce => "??" + } +} + +type OperatorRealizationRefusal + = NoStructuralOperationDeclared { declaration: DeclarationRef, operator: BinOp } + | StructuralOrderingDuplicated { declaration: DeclarationRef, row_count: Int } + | OperandIdentityUnavailableAt { operator: BinOp, facts: OperandShapeFacts } + +type OperatorRealization + = HostOperator + | StructuralEquality { declaration: DeclarationRef } + | StructuralComparison { declaration: DeclarationRef, binding: StructuralOrderingBinding, test: OrderingTest } + | OperatorRealizationRefused { cause: OperatorRealizationRefusal } + +fn operator_realization_refusal_message(cause: OperatorRealizationRefusal) -> String { + match cause { + NoStructuralOperationDeclared { declaration: d, operator: o } => + concat( + "operator realization: host operator `", binop_label(op: o), "` on structural operand ", + d.module_path as String, ".", d.decl_name as String, + " -- the declaration has no host realization and declares no operation for this operator; spell the operation as a call to the declared structural operation" + ) + StructuralOrderingDuplicated { declaration: d, row_count: n } => + concat( + "operator realization: structural ordering for ", + d.module_path as String, ".", d.decl_name as String, + " has more than one declared comparison (gunbc.structural_realization_bindings authoring defect)" + ) + OperandIdentityUnavailableAt { operator: o, facts: f } => + concat( + "operator realization: host operator `", binop_label(op: o), "` on an operand whose declaration could not be read", + " (authored `", f.authored_name, "`, connective ", f.connective, ", children ", to_string(value: f.child_count), + ", resolved ", if f.resolved { "yes" } else { "no" }, ", decl_file `", f.decl_file, "`)" + ) + } +} + +// THE DECISION, arm by arm, each stating what it is keyed on. +// +// NULL-COALESCING never reaches this fold from the Rust emitter: emit_typed_bin_op answers it from +// emit_null_coalesce before asking for a realization, because its operand is an Optional carrier and +// the question is cardinality, not operand structure. Its arm here is the fold's totality over the +// closed BinOp vocabulary, not a second decision about it. +// +// LOGICAL CONNECTIVES answer HostOperator on a structural operand, and that arm is HONEST ABOUT +// WHAT IT DOES NOT CHECK. Inference types `&&`/`||` as returning Bool without constraining its +// OPERANDS to be one (v1.compiler.types infer_binop_type_node: the And and Or arms name only the +// result), so `a && b` with a Peano-shaped `a` is authorable and this arm would emit the host token +// for it. It is not repaired by refusing every structural operand: v2.std.logic Bool is a declared +// structural coproduct that 593 modules import as their ordinary Bool, so a blanket refusal would +// refuse the corpus's ordinary conjunction -- the wall paid for in false refusals. The repair is a +// declared-connective row family beside the ordering rows, and it is a DECLARED STALL with that +// trigger (gunbc.structural_realization_bindings structural_connective_stall), not a claim this +// authority already covers connectives. +// +// AN OPERAND WHOSE DECLARATION COULD NOT BE READ is not a widen and not a guess: it decides by +// operator class, below. +fn operator_realization_for( + op: BinOp, + operand: OperandRealization, + ordering_rows: List +) -> OperatorRealization { + match operand { + HostNumericOperand => HostOperator + HostRealizedOperand { reason: _ } => HostOperator + OperandIdentityUnavailable { facts: f } => + match op { + Eq => HostOperator + Ne => HostOperator + And => HostOperator + Or => HostOperator + NullCoalesce => HostOperator + Lt => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Gt => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Le => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Ge => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Add => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Sub => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Mul => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Div => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + Mod => OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: op, facts: f } } + } + StructuralOperand { declaration: d } => + match op { + Eq => StructuralEquality { declaration: d } + Ne => StructuralEquality { declaration: d } + Lt => structural_ordering_realization(op: op, declaration: d, ordering_rows: ordering_rows) + Gt => structural_ordering_realization(op: op, declaration: d, ordering_rows: ordering_rows) + Le => structural_ordering_realization(op: op, declaration: d, ordering_rows: ordering_rows) + Ge => structural_ordering_realization(op: op, declaration: d, ordering_rows: ordering_rows) + And => HostOperator + Or => HostOperator + NullCoalesce => HostOperator + Add => structural_arithmetic_refusal(op: op, declaration: d) + Sub => structural_arithmetic_refusal(op: op, declaration: d) + Mul => structural_arithmetic_refusal(op: op, declaration: d) + Div => structural_arithmetic_refusal(op: op, declaration: d) + Mod => structural_arithmetic_refusal(op: op, declaration: d) + } + } +} + +fn structural_arithmetic_refusal(op: BinOp, declaration: DeclarationRef) -> OperatorRealization { + OperatorRealizationRefused { cause: NoStructuralOperationDeclared { declaration: declaration, operator: op } } +} + +// An ordering operator on a structural operand: the declared comparison, or the refusal. Reached +// only from the four ordering arms above, so an op with no ordering test is a refusal here too -- +// that arm is unreachable by construction, not a wildcard. +fn structural_ordering_realization(op: BinOp, declaration: DeclarationRef, ordering_rows: List) -> OperatorRealization { + match ordering_test_for(op: op) { + Absent => structural_arithmetic_refusal(op: op, declaration: declaration) + Present { value: test } => + match structural_ordering_for(rows: ordering_rows, carrier: declaration) { + StructuralOrderingFound { row: row } => StructuralComparison { declaration: declaration, binding: row, test: test } + StructuralOrderingAbsent => structural_arithmetic_refusal(op: op, declaration: declaration) + StructuralOrderingAmbiguous { row_count: n } => OperatorRealizationRefused { cause: StructuralOrderingDuplicated { declaration: declaration, row_count: n } } + } + } +} diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index e63d38d3311..d36cbadaa45 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -38,16 +38,24 @@ fn violation_count(source: String, wanted: String) -> Int { // which is the whole point of enrolling it: DESIGN 4b(4) keeps the evidence after a climb // precisely so the higher rung stays real. -// RED, AND CURRENTLY FAILING -- ENROLLED IN v2.workflow.floor_expected_red rather than fixed. -// A kernel integer at the PEANO Nat. 5 is not Zero and not Succ and no realization row covers -// src/v2/std/nat.dag, so this OUGHT to refuse. It does not, and the control run on 2026-08-23 -// establishes that it never did: gunbc built from origin/main 907f19c2cc7 admits this source -// exactly as the branch does. The refusal was ASSERTED here, not broken by this change. -// The enrolment row carries the full branch-and-main control table and the next-rung trigger. +// A kernel integer at the PEANO Nat -- RULED ADMITTED THROUGH THE DECLARED HOMOMORPHISM, and this +// row's claim changed with the ruling (XL-0N, adhoc-aec65f93-b00, operator ruling 2026-08-30). +// This row used to assert a refusal (5 is not Zero and not Succ) and sat in +// v2.workflow.floor_expected_red with the trigger "the expected-type-directed literal introduction +// judgment -- the MODEL half -- is NOT built". It is built: std.literal_elaboration elaborates the +// kernel literal at the exact v2.std.nat.Nat boundary through the ONE declared Peano homomorphism +// (gunbc.structural_realization_bindings) into Succ^5(Zero), typed as the destination, so the +// value the inhabitance judgment sees IS a Nat. Admission here is therefore the ruled answer, and +// this row is the positive control for it. The DISCRIMINATING evidence -- that the literal is +// elaborated rather than merely waved through -- is the emitted-bytes witness +// test.claim.self_host_peano_literal_operator_realization_witness_test +// w_literal_at_peano_argument_boundary_emits_its_image, whose forbidden token is exactly the bare +// digit this probe used to carry; the two rows are read together. DESIGN 4b(4): the probe flips +// to a permanent regression control, it does not retire. data peano_nat_arg_source: String = "module probe_inhabit_peano\nimport v2.std.nat { Nat }\nfn takes_peano(n: Nat) -> Int { 1 }\nfn probe() -> Int { takes_peano(n: 5) }\n" -test fn w_kernel_numeric_at_the_peano_nat_is_refused() -> Bool { - violation_count(source: peano_nat_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 +test fn w_kernel_numeric_at_the_peano_nat_is_admitted_through_its_homomorphism() -> Bool { + violation_count(source: peano_nat_arg_source, wanted: "DeclaredTypeNotInhabited") == 0 } // GREEN -- the same literal at the NATIVE Nat. Structurally this is a kernel value at an diff --git a/dag/test/claim/self_host_peano_literal_operator_realization_witness_test.dag b/dag/test/claim/self_host_peano_literal_operator_realization_witness_test.dag new file mode 100644 index 00000000000..3341724f584 --- /dev/null +++ b/dag/test/claim/self_host_peano_literal_operator_realization_witness_test.dag @@ -0,0 +1,155 @@ +module test.claim.self_host_peano_literal_operator_realization_witness_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE EMITTED-BYTES HALF OF THE STRUCTURAL PEANO NAT FALSIFIERS (XL-0N, adhoc-aec65f93-b00). +// Each row compiles a virtual module through the PRODUCTION v1 emitter (compile_dag_rust_emit_check) +// and asserts on the Rust it writes. The interpreter-executed half -- the declared structural +// operations on nontrivial Succ values and the generic decisions by row and identity -- is +// v2.test.claim.self_host.peano_nat_structural_realization_test. +// +// The required images are spelled in the emitter's record-literal layout (emit_typed_record_lit: +// one field per line, four-space indent, the closing brace at column zero), read off the same +// probes compiled with the lane's fixed-point binary; a single-line spelling never matches. +// The forbidden tokens are the emitter's rendering BEFORE this lane, read off the same probes +// compiled with the pre-lane binary (recorded here so a reader can see what each row turns red on): +// arg boundary crate::v2_std_nat::nat_add(n.clone(), 2) -> E0308 Rc vs integer +// return boundary -> Rc {\n 2\n} -> E0308 +// literal equality (a.clone() == 3) -> E0308 +// ordering (a.clone() < b.clone()) -> E0369 on Rc +// arithmetic (a.clone() / b.clone()) -> E0369 on Rc +// The two host-control rows pin that the SAME operators on a native i64 operand keep the host +// token and the bare digit: the decision is keyed on the operand's declaration, not the spelling. + +// A kernel integer literal at a v2.std.nat.Nat ARGUMENT boundary elaborates to its Zero/Succ +// image (std.literal_elaboration PeanoUnfold, the row in gunbc.structural_realization_bindings). +test fn w_literal_at_peano_argument_boundary_emits_its_image() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_arg_probe\nimport std.types { Bool }\nimport v2.std.nat { Nat, nat_add }\nfn probe(n: Nat) -> Nat { nat_add(a: n, b: 2) }\n", + "src/test_claim_peano_arg_probe.rs", + ["Nat::Succ {\n prev: Rc::new(Nat::Succ {\n prev: Rc::new(Nat::Zero),\n})"], + [", 2)"] + ) +} + +// The same at a declared RETURN boundary. +test fn w_literal_at_peano_return_boundary_emits_its_image() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_return_probe\nimport v2.std.nat { Nat }\nfn probe() -> Nat { 2 }\n", + "src/test_claim_peano_return_probe.rs", + ["Nat::Succ {\n prev: Rc::new(Nat::Succ {\n prev: Rc::new(Nat::Zero),\n})"], + ["{\n 2\n}"] + ) +} + +// The other OPERAND of a binary operator is a boundary: `a == 3` with a: Nat introduces 3 at Nat, +// and equality on the Peano operand is structural (the emitted enum derives PartialEq). +test fn w_literal_operand_of_peano_equality_emits_its_image() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_literal_eq_probe\nimport std.types { Bool }\nimport v2.std.nat { Nat }\nfn probe(a: Nat) -> Bool { a == 3 }\n", + "src/test_claim_peano_literal_eq_probe.rs", + ["== Rc::new(Nat::Succ {\n prev: Rc::new(Nat::Succ {\n prev: Rc::new(Nat::Succ {\n prev: Rc::new(Nat::Zero),\n})"], + ["== 3)"] + ) +} + +// Zero is the image of 0: the nullary constructor, not a digit. +test fn w_zero_literal_emits_the_nullary_constructor() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_zero_probe\nimport v2.std.nat { Nat }\nfn probe() -> Nat { 0 }\n", + "src/test_claim_peano_zero_probe.rs", + ["Rc::new(Nat::Zero)"], + ["{\n 0\n}"] + ) +} + +// An ORDERING on Peano operands is a call to the declared comparison tested against std.algebra +// Ordering (std.operator_realization StructuralComparison), never the host `<`. +test fn w_ordering_on_peano_operands_calls_the_declared_comparison() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_lt_probe\nimport std.types { Bool }\nimport v2.std.nat { Nat }\nfn probe(a: Nat, b: Nat) -> Bool { a < b }\n", + "src/test_claim_peano_lt_probe.rs", + ["(crate::v2_std_nat::nat_compare(a.clone(), b.clone()) == crate::std_algebra::Ordering::Less)"], + [" < "] + ) +} + +// A non-strict ordering negates the opposite variant: `<=` is `!= Greater`. +test fn w_non_strict_ordering_negates_the_opposite_variant() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_le_probe\nimport std.types { Bool }\nimport v2.std.nat { Nat }\nfn probe(a: Nat, b: Nat) -> Bool { a <= b }\n", + "src/test_claim_peano_le_probe.rs", + ["(crate::v2_std_nat::nat_compare(a.clone(), b.clone()) != crate::std_algebra::Ordering::Greater)"], + [" <= "] + ) +} + +// FORCING HOST ARITHMETIC ONTO PEANO OPERANDS REDS IN THE BYTES: infix `/` on Nat is refused by +// a typed compile_error naming the declaration and the operator, not emitted as a token rustc +// refuses later under E0369. +test fn w_host_arithmetic_on_peano_operands_refuses_in_the_bytes() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.peano_div_probe\nimport v2.std.nat { Nat }\nfn probe(a: Nat, b: Nat) -> Nat { a / b }\n", + "src/test_claim_peano_div_probe.rs", + ["compile_error!(\"operator realization: host operator `/` on structural operand v2.std.nat.Nat"], + [" / "] + ) +} + +// THE BOOL ROW ON THE EMITTED PATH: a kernel true at a v2.std.logic.Bool boundary emits the +// structural constructor. (The interpreter realizes Bool natively and never executes this image; +// the emitted bytes are the only place the image exists, so this row is its whole evidence.) +test fn w_kernel_bool_at_structural_bool_boundary_emits_its_constructor() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.structural_bool_probe\nimport v2.std.logic { Bool }\nfn probe() -> Bool { true }\nfn probe_false(b: Bool) -> Bool { false }\n", + "src/test_claim_structural_bool_probe.rs", + ["Bool::True", "Bool::False"], + ["{\n true\n}", "{\n false\n}"] + ) +} + +// HOST CONTROL for the Bool row: the prelude std.types Bool realizes natively and keeps the host +// keyword -- a rule keyed on the spelling `Bool` cannot pass this row and the one above together. +test fn w_kernel_bool_at_native_bool_boundary_stays_the_keyword() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.native_bool_probe\nimport std.types { Bool }\nfn probe() -> Bool { true }\n", + "src/test_claim_native_bool_probe.rs", + ["{\n true\n}"], + ["Bool::True"] + ) +} + +// HOST CONTROL: the same ordering on a native i64 operand keeps the host token. Without this row +// a realization that routed EVERY `<` through a comparison call would pass the Peano rows. +test fn w_ordering_on_native_operands_keeps_the_host_operator() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.native_lt_probe\nimport std.types { Bool, Int }\nfn probe(a: Int, b: Int) -> Bool { a < b }\n", + "src/test_claim_native_lt_probe.rs", + ["(a.clone() < b.clone())"], + ["nat_compare", "compile_error!"] + ) +} + +// HOST CONTROL: a literal at a native Int boundary stays the bare digit (DirectLiteral). +test fn w_literal_at_native_boundary_stays_direct() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.native_literal_probe\nimport std.types { Int }\nfn probe(a: Int) -> Int { a + 2 }\n", + "src/test_claim_native_literal_probe.rs", + ["(a.clone() + 2)"], + ["Succ", "Zero"] + ) +} + +// SAME SPELLING, DIFFERENT DECLARATION: std.nat Nat is the native-realizing semiring alias, and a +// literal at ITS boundary stays direct while the host `<` stays the host token. This is the row a +// spelling-keyed decision cannot pass together with the Peano rows above. +test fn w_native_nat_declaration_keeps_direct_literal_and_host_operator() -> Bool { + compile_dag_rust_emit_check( + "module test.claim.native_nat_probe\nimport std.types { Bool }\nimport std.nat { Nat }\nfn probe(a: Nat) -> Bool { a < 2 }\n", + "src/test_claim_native_nat_probe.rs", + ["(a.clone() < 2)"], + ["Succ", "nat_compare", "compile_error!"] + ) +} diff --git a/scratch-probe/test/claim/peano_probe.dag b/scratch-probe/test/claim/peano_probe.dag new file mode 100644 index 00000000000..5404778f153 --- /dev/null +++ b/scratch-probe/test/claim/peano_probe.dag @@ -0,0 +1,12 @@ +module test.claim.peano_probe +import std.types { Int, Bool } +import v2.std.nat { Nat, Zero, Succ, nat_add } +fn arg_boundary(n: Nat) -> Nat { nat_add(a: n, b: 2) } +fn return_boundary() -> Nat { 2 } +fn ordering(a: Nat, b: Nat) -> Bool { a < b } +fn ordering_le(a: Nat, b: Nat) -> Bool { a <= b } +fn equality(a: Nat, b: Nat) -> Bool { a == b } +fn literal_equality(a: Nat) -> Bool { a == 3 } +fn arithmetic(a: Nat, b: Nat) -> Nat { a / b } +fn host_ordering(a: Int, b: Int) -> Bool { a < b } +fn host_literal(a: Int) -> Int { a + 2 } diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index e1170568150..0618f9ee734 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -8,6 +8,8 @@ import std.syntax { AlgebraFieldKind, AlgAdd, AlgMul, AlgReciprocal, AlgQuotient, AlgRemainder, AlgCompare, AlgMeet, AlgJoin } import std.algebra { CollectionSizeEffect, CostShape, AlgebraFieldTemplate } +import std.literal_elaboration { LiteralElaboration } +import std.operator_realization { OperandDeclaration } import std.induction { SubValueRelation } import std.occurrence_identity { NodeOccurrenceIdentity, @@ -165,6 +167,7 @@ type ExprErrorKind = ParseRecoveryError | SemanticExprError | InternalExprError type ExprData = NoExprData | ExprLiteral { value: LiteralValue } + | ExprElaboratedLiteral { value: LiteralValue, elaboration: LiteralElaboration } | ExprError { kind: ExprErrorKind, message: String } | ExprVar { binding_kind: VarBindingKind? } | ExprFieldAccess { summary: FieldSummary? } @@ -175,7 +178,7 @@ type ExprData | ExprLet | ExprRecordLit { parent_enum: String? } | ExprListLit - | ExprBinOp { op: BinOp, algebra_field: AlgebraFieldKind? } + | ExprBinOp { op: BinOp, algebra_field: AlgebraFieldKind?, operand: OperandDeclaration? } | ExprUnaryOp { op: UnaryOpKind } | ExprLambda | ExprStringInterp @@ -1650,6 +1653,11 @@ fn expr_literal_int_optional(expr: Node) -> Int? { LitInt { value: v } => Present { value: v } _ => none } + ExprElaboratedLiteral { value: lit, elaboration: _ } => + match lit { + LitInt { value: v } => Present { value: v } + _ => none + } ExprUnaryOp { op: Neg } => match expr_literal_int_optional(expr: unaryop_operand(texpr: expr)) { Present { value: v } => Present { value: 0 - v } @@ -1688,6 +1696,7 @@ fn expr_is_any_literal(expr: Node) -> Bool { LitNull => false _ => true } + ExprElaboratedLiteral { value: _, elaboration: _ } => true ExprUnaryOp { op: Neg } => expr_is_any_literal(expr: unaryop_operand(texpr: expr)) _ => false } @@ -1918,6 +1927,7 @@ fn expr_has_non_tail_self_call(texpr: Node, fn_name: String, in_tail: Bool, sour ExprError { kind: _, message: _ } => false ExprVar { binding_kind: _ } => false ExprLiteral { value: _ } => false + ExprElaboratedLiteral { value: _, elaboration: _ } => false ExprFieldAccess { summary: _ } => texpr.children |> any(child => expr_has_non_tail_self_call(texpr: child, fn_name: fn_name, in_tail: false, source_indices: source_indices)) ExprMethodCall { method_semantics: _ } => diff --git a/src/v1/02_parse.dag b/src/v1/02_parse.dag index 7e21620ee40..c6cf9ae447f 100644 --- a/src/v1/02_parse.dag +++ b/src/v1/02_parse.dag @@ -4623,7 +4623,7 @@ fn parse_expr_loop(tokens: TokenStream, ctx: ParseContext, lhs: Node, min_bp: In match binop_opt { Present { value: binop } => { let minted = mint_parsed_node_identity(ctx: r.ctx) - let new_lhs = make_expr_node(occurrence_identity: minted.identity, expr_data: ExprBinOp { op: binop, algebra_field: none }, children: [lhs, r.expr], inferred: none, span: loop_span) + let new_lhs = make_expr_node(occurrence_identity: minted.identity, expr_data: ExprBinOp { op: binop, algebra_field: none, operand: none }, children: [lhs, r.expr], inferred: none, span: loop_span) parse_expr_loop(tokens: r.tokens, ctx: minted.ctx, lhs: new_lhs, min_bp: min_bp) } Absent => ExprResult { expr: lhs, tokens: r.tokens, ctx: r.ctx, err: Present { value: parse_error(msg: concat("unknown binary operator: ", op_tok.text), span: loop_span) } } @@ -5279,7 +5279,7 @@ fn parse_expr_loop_no_brace(tokens: TokenStream, ctx: ParseContext, lhs: Node, m match binop_opt { Present { value: binop } => { let minted = mint_parsed_node_identity(ctx: r.ctx) - let new_lhs = make_expr_node(occurrence_identity: minted.identity, expr_data: ExprBinOp { op: binop, algebra_field: none }, children: [lhs, r.expr], inferred: none, span: loop_span) + let new_lhs = make_expr_node(occurrence_identity: minted.identity, expr_data: ExprBinOp { op: binop, algebra_field: none, operand: none }, children: [lhs, r.expr], inferred: none, span: loop_span) parse_expr_loop_no_brace(tokens: r.tokens, ctx: minted.ctx, lhs: new_lhs, min_bp: min_bp) } Absent => ExprResult { expr: lhs, tokens: r.tokens, ctx: r.ctx, err: Present { value: parse_error(msg: concat("unknown binary operator: ", op_tok.text), span: loop_span) } } diff --git a/src/v1/04_env.dag b/src/v1/04_env.dag index 160075169a5..f85c9dedca8 100644 --- a/src/v1/04_env.dag +++ b/src/v1/04_env.dag @@ -2,10 +2,12 @@ module v1.compiler.infer_env import std.occurrence_identity { OccurrenceSynthetic } -import v1.std.core { Node, NewlineIndex, InternTable, empty_intern_table, merge_intern_tables, intern, intern_find, intern_str, source_text_at, authored_name_at, find_child_named, Cardinality, Connective, ExprData, InferredNode, kernel_span, module_path_segments, param_node_name_at, param_node_type_expr, CompilerDiagnostic, AmbiguousReference, UnresolvedType } +import v1.std.core { Node, NewlineIndex, InternTable, Resolved, qualified_last_segment, empty_intern_table, merge_intern_tables, intern, intern_find, intern_str, source_text_at, authored_name_at, find_child_named, Cardinality, Connective, ExprData, InferredNode, kernel_span, module_path_segments, param_node_name_at, param_node_type_expr, CompilerDiagnostic, AmbiguousReference, UnresolvedType } import v1.compiler.type_head_exposure { TypeHeadExposure } import std.types { SourceSpan, is_kernel_type } +import std.decl_ref { decl_ref, DeclarationRef } +import std.operator_realization { OperandDeclaration } import std.induction { InductiveField, RecursionShape, DirectRecursion, ListRecursion, OptionalRecursion, SetRecursion, MapValueRecursion, SubValueRelation, SubValueUnknown, PreservedValue } import std.algebra { FreeMonoid, Empty, Cons } @@ -1283,3 +1285,66 @@ fn env_with_type_variable_bindings(env: TypeEnv, tp_names: List) -> Type } ) } + +// THE EXACT PATH, AT ANY CONSUMER (relocated from v1.compiler.emit_rust, XL-0N). A type reference +// carries its resolved declaration (`inferred: Resolved { node }`); the declaration's module is the +// containment fact the corpus-wide bare-name census already holds (SymbolIndex.global_bare, one row +// per declared name with its module_path and the declaration node), so the DeclarationRef is read +// from that census by identity -- the candidate whose declaration node IS the resolved node, by +// ident_span -- and never minted from a spelling. Identity the census cannot supply (a kernel mint, +// a variant alias, an unresolved reference) is absent. +fn binding_declares_span(binding: TypeBinding, sp: SourceSpan) -> Bool { + match binding.resolved.ident_span { + Present { value: s } => s.file == sp.file && s.start == sp.start + Absent => false + } +} + +// A reference the resolver leaves IN PLACE -- a recursive type such as v2.std.nat Nat, whose leaf arm +// answers `resolved: n` with no inferred node (v1.compiler.resolve resolve_node, is_recursive_type_for) +// -- still names its declaration: the env binding the resolver established for the reference's ident +// (lookup_type_for) carries the declaration's own ident_span, which is the span the global roster is +// matched on. Without this arm every recursive destination answered Absent here and fell to the +// identity-unavailable arms downstream (measured: the Peano literal and ordering rows passed for +// v2.std.logic Bool and failed for v2.std.nat Nat on the same compiler). The ident-keyed lookup is +// scoped: a parameter's type reference is bound in its function's scope, so this read is correct +// at inference and NOT at emission, where only the module env survives. A by-name arm was tried +// here for the emitter and refuted: the module-visible name is answered by pool precedence, so it +// returned std.nat.Nat for a module that imported v2.std.nat.Nat, and the span match then confirmed +// that homonym exactly. The reading is therefore done once, at inference, and carried on the typed +// tree (std.operator_realization OperandDeclaration on ExprBinOp) for emission to consume. +fn type_reference_declaration(n: Node, source_indices: Map, env: TypeEnv) -> OperandDeclaration? { + let rt = match n.inferred { + Present { value: Resolved { node: r } } => r + _ => + match lookup_type_for(env: env, node: n) { + Present { value: bound } => bound + Absent => n + } + } + let decl_name = qualified_last_segment(name: authored_name_at(source_indices: source_indices, node: rt)) + if decl_name == "" { return none } + match rt.ident_span { + Absent => none + Present { value: sp } => + match map_get(env.symbol_index.global_bare, decl_name) { + Present { value: GlobalBareUniqueBinding { module_path: mp, binding: b } } => + if binding_declares_span(binding: b, sp: sp) { + Present { value: OperandDeclaration { declaration: decl_ref(module_path: mp, decl_name: decl_name), decl_file: sp.file } } + } else { none } + Present { value: GlobalBareAmbiguousBinding { candidates: cands } } => + match cands |> filter(c => binding_declares_span(binding: c.binding, sp: sp)) |> first { + Present { value: c } => Present { value: OperandDeclaration { declaration: decl_ref(module_path: c.module_path, decl_name: decl_name), decl_file: sp.file } } + Absent => none + } + Absent => none + } + } +} + +fn type_reference_declaration_ref(n: Node, source_indices: Map, env: TypeEnv) -> DeclarationRef? { + match type_reference_declaration(n: n, source_indices: source_indices, env: env) { + Present { value: od } => Present { value: od.declaration } + Absent => none + } +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index b917f8bff1a..d16b4029354 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -8,7 +8,15 @@ import std.content_hash { content_hash_validate_lower_hex_length, } import extdeps.container.oci.digest { oci_other_digest_algorithm, oci_other_digest_encoded } -import std.syntax { Add, BinOp, LitStr, LiteralValue } +import std.syntax { Add, BinOp, LitStr, LitInt, LitBool, LiteralValue } +import std.decl_ref { DeclarationRef } +import std.operator_realization { OperandDeclaration } +import std.literal_elaboration { + LiteralElaboration, LiteralHomomorphism, LiteralUnfolding, PeanoUnfold, BooleanUnfold, + LiteralElaborationOutcome, DirectLiteral, ViaHomomorphism, LiteralElaborationRefused, + elaborate_literal_at, literal_source_kind_of, literal_elaboration_refusal_message +} +import gunbc.structural_realization_bindings { literal_homomorphism_rows } import std.coercion { dag_can_cast, is_dag_cast_domain_type } import v1.compiler.type_head_exposure { TypeHeadView, KernelScalarHead, ApplicationHead, ProductHead, CoproductHead, CallableHead, @@ -26,7 +34,7 @@ import v1.std.core { field_node_type_expr, field_node_name_at, Connective, Conj, Disj, NoConnective, Arrow, ExprData, NoExprData, - ExprLiteral, ExprError, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, + ExprLiteral, ExprElaboratedLiteral, ExprError, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, ExprMatch, ExprIf, ExprLet, ExprRecordLit, ExprListLit, ExprBinOp, ExprUnaryOp, ExprLambda, ExprStringInterp, ExprBlock, ExprCast, ExprForEach, ExprIndex, ExprSlice, ExprReturn, @@ -116,7 +124,7 @@ import v1.compiler.infer_env { qualify_borrowed_type_names, qualify_borrowed_inferred, qualified_all_but_last, env_with_type_variable_bindings, GlobalBareCandidate, node_with_inferred, node_with_children, ServiceCensusEntry, qualify_decl_reference_positions, - lookup_binding_by_name, binding_declares_name, + lookup_binding_by_name, binding_declares_name, type_reference_declaration_ref, type_reference_declaration, listed_import_required_bare_call_blocked, effective_visible_binding, unit_variant_index_shadow_insert, build_unit_variant_index, UnitVariantContribution @@ -4967,11 +4975,201 @@ fn qualified_value_projection(texpr: Node, scope: InferScope, span: SourceSpan) // which is exactly how the deleted `func_sig_if_resolved` came to erase the ambiguity in // the first place. + +// --------------------------------------------------------------------------------------------- +// LITERAL ELABORATION AT A TYPED BOUNDARY (std.literal_elaboration; XL-0N, adhoc-aec65f93-b00). +// +// The literal arm below receives the boundary's expected type at every position that supplies one +// -- call argument, declared return, record field, data initializer, annotated let, list element, +// map value, block tail, and (via infer_binop_operands) the other operand of a binary operator -- +// and asks ONE judgment: does the destination declaration supply this kernel literal through a +// declared homomorphism? When it does, the literal is REPLACED in the typed tree by an +// ExprElaboratedLiteral whose record names the source kind, the exact destination and the selected +// homomorphism, and whose single child is the literal's IMAGE under that homomorphism -- ordinary +// constructor nodes of the destination (Zero / Succ { prev: ... } for the Peano unfolding), typed +// as the destination. Emission renders the image the way it renders any constructor and never +// re-decides from spelling, imports, or the host compiler's expectations. +// +// Identity, not spelling: the destination is read by type_reference_declaration_ref (the same +// exact-identity reader the Rust renderer uses), so std.nat Nat and v2.std.nat Nat -- one spelling, +// two declarations -- take different arms by construction. A destination the census cannot +// identify, an optional-cardinality boundary, and a destination with no row all leave the literal +// exactly as it was (DirectLiteral); the inhabitance judgment owns any refusal there. +// --------------------------------------------------------------------------------------------- + +type LiteralBoundary + = LiteralBoundaryPlain + | LiteralBoundaryElaborated { elaboration: LiteralElaboration, destination_type: Node } + | LiteralBoundaryRefused { message: String } + +fn literal_boundary_elaboration(lit: LiteralValue, expected: Node?, scope: InferScope) -> LiteralBoundary { + match expected { + Absent => LiteralBoundaryPlain + Present { value: exp } => + if exp.return_cardinality == CardOptional { + LiteralBoundaryPlain + } else { + match type_reference_declaration_ref(n: exp, source_indices: scope.type_env.source_indices, env: scope.type_env) { + Absent => LiteralBoundaryPlain + Present { value: destination } => + let kind = literal_source_kind_of(value: lit) + let natively = decl_file_realizes_natively(decl_file: type_reference_decl_file(n: exp)) + match elaborate_literal_at(rows: literal_homomorphism_rows, source_kind: kind, destination: destination, destination_realizes_natively: natively) { + DirectLiteral => LiteralBoundaryPlain + ViaHomomorphism { homomorphism: h } => + LiteralBoundaryElaborated { + elaboration: LiteralElaboration { source_kind: kind, destination: destination, homomorphism: h }, + destination_type: exp + } + LiteralElaborationRefused { cause: c } => + LiteralBoundaryRefused { message: literal_elaboration_refusal_message(cause: c) } + } + } + } + } +} + +// The image's nodes carry a synthetic ident_span whose file is not a source index, so every +// name reader (authored_name_at) answers from the node's own name -- the constructor names come +// from the homomorphism row, never from source text. +fn elaborated_span(name: String) -> SourceSpan { + SourceSpan { file: "", start: 0, end: string_length(s: name) } +} + +fn elaborated_expr_node(name: String, expr_data: ExprData, children: List, destination_type: Node, span: SourceSpan) -> Node { + Node { + occurrence_identity: OccurrenceSynthetic, + name: name, span: span, ident_span: Present { value: elaborated_span(name: name) }, children: children, + connective: NoConnective, + params: [], inferred: Present { value: Resolved { node: destination_type } }, return_cardinality: Required, + uses: [], body: none, transport: none, properties: [], + type_annotation: none, is_self_recursive: false, + has_non_tail_self_call: false, match_pattern: none, expr_data: expr_data + } +} + +fn unfold_peano_image(n: Int, zero: String, succ: String, prev_field: String, parent: String, destination_type: Node, span: SourceSpan) -> Node { + if n <= 0 { + elaborated_expr_node( + name: zero, + expr_data: ExprVar { binding_kind: Present { value: VariantValueBinding { parent_enum: parent } } }, + children: [], destination_type: destination_type, span: span + ) + } else { + let prev = unfold_peano_image(n: n - 1, zero: zero, succ: succ, prev_field: prev_field, parent: parent, destination_type: destination_type, span: span) + let field = make_field_init_node(occurrence_identity: OccurrenceSynthetic, name: prev_field, value: prev, span: span, name_span: elaborated_span(name: prev_field)) + elaborated_expr_node( + name: succ, + expr_data: ExprRecordLit { parent_enum: Present { value: parent } }, + children: [field], destination_type: destination_type, span: span + ) + } +} + +fn unfold_literal_image(lit: LiteralValue, elaboration: LiteralElaboration, destination_type: Node, span: SourceSpan) -> Node { + match elaboration.homomorphism.producer { + PeanoUnfold { zero: zero, succ: succ, prev_field: prev_field } => + match lit { + LitInt { value: n } => + unfold_peano_image( + n: n, + zero: zero.decl_name as String, succ: succ.decl_name as String, prev_field: prev_field as String, + parent: elaboration.destination.decl_name as String, + destination_type: destination_type, span: span + ) + _ => make_expr_error_node(occurrence_identity: OccurrenceSynthetic, kind: InternalExprError, message: "literal elaboration: a Peano unfolding row was selected for a non-integer literal (gunbc.structural_realization_bindings keys the row on KernelIntLiteral, so this row is malformed)", span: span) + } + BooleanUnfold { true_variant: t, false_variant: f } => + match lit { + LitBool { value: b } => + elaborated_expr_node( + name: if b { t.decl_name as String } else { f.decl_name as String }, + expr_data: ExprVar { binding_kind: Present { value: VariantValueBinding { parent_enum: elaboration.destination.decl_name as String } } }, + children: [], destination_type: destination_type, span: span + ) + _ => make_expr_error_node(occurrence_identity: OccurrenceSynthetic, kind: InternalExprError, message: "literal elaboration: a Boolean unfolding row was selected for a non-boolean literal (gunbc.structural_realization_bindings keys the row on KernelBoolLiteral, so this row is malformed)", span: span) + } + } +} + +// A binary operator's operands are a typed boundary for each other: a literal operand is +// introduced at the OTHER operand's resolved type (`digit == 0` with digit: v2.std.nat.Nat asks +// the Peano row for 0). Only a literal operand takes the other's type as expected -- every other +// operand shape is inferred exactly as before -- and it takes it through infer_expr_body, not the +// refinement-checking infer_expr wrapper, because comparing against a literal is not a refinement +// boundary (`x == 0` with x refined positive is a legitimate test, not an assignment). +type BinopOperands { + left: InferResult + right: InferResult +} + +// THE LEFT OPERAND'S DECLARATION, read here where the reference's scoped binding is live, after +// hopping a where-refinement to its base (`type Char = Int where ...` realizes as Int): the fact +// std.operator_realization decides on, stamped on the ExprBinOp node for emission. Absent when the +// operand's type node names no declaration (an inference-synthesized node), which emission answers +// by operator class. +fn operand_declaration_of_type(rt: Node, scope: InferScope, fuel: Int) -> OperandDeclaration? { + if fuel > 0 && is_where_refinement_type(ty: rt) { + match rt.children |> first { + Present { value: base } => + let base_resolved = match lookup_type_for(env: scope.type_env, node: base) { + Present { value: r } => r + Absent => base + } + operand_declaration_of_type(rt: base_resolved, scope: scope, fuel: fuel - 1) + Absent => type_reference_declaration(n: rt, source_indices: scope.type_env.source_indices, env: scope.type_env) + } + } else { + type_reference_declaration(n: rt, source_indices: scope.type_env.source_indices, env: scope.type_env) + } +} + +fn infer_operand_literal(lit_expr: Node, other: Node, scope: InferScope) -> InferResult { + let other_type = match other.inferred { + Present { value: Resolved { node: rt } } => Present { value: rt } + _ => none + } + infer_expr_body(texpr: lit_expr, scope: scope, expected: other_type) +} + +fn infer_binop_operands(left_expr: Node, right_expr: Node, scope: InferScope) -> BinopOperands { + let left_is_literal = expr_is_any_literal(expr: left_expr) + let right_is_literal = expr_is_any_literal(expr: right_expr) + if right_is_literal && !left_is_literal { + let l = infer_expr(texpr: left_expr, scope: scope, expected: none) + BinopOperands { left: l, right: infer_operand_literal(lit_expr: right_expr, other: l.typed, scope: scope) } + } else if left_is_literal && !right_is_literal { + let r = infer_expr(texpr: right_expr, scope: scope, expected: none) + BinopOperands { left: infer_operand_literal(lit_expr: left_expr, other: r.typed, scope: scope), right: r } + } else { + BinopOperands { + left: infer_expr(texpr: left_expr, scope: scope, expected: none), + right: infer_expr(texpr: right_expr, scope: scope, expected: none) + } + } +} + fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResult { match texpr.expr_data { ExprLiteral { value: lit } => let span = texpr.span - ok_infer(texpr: make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprLiteral { value: lit }, children: [], inferred: Present { value: Resolved { node: infer_literal_node(lit: lit) } }, span: span)) + let plain = make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprLiteral { value: lit }, children: [], inferred: Present { value: Resolved { node: infer_literal_node(lit: lit) } }, span: span) + match literal_boundary_elaboration(lit: lit, expected: expected, scope: scope) { + LiteralBoundaryPlain => ok_infer(texpr: plain) + LiteralBoundaryElaborated { elaboration: e, destination_type: dt } => + ok_infer(texpr: make_expr_node( + occurrence_identity: texpr.occurrence_identity, + expr_data: ExprElaboratedLiteral { value: lit, elaboration: e }, + children: [unfold_literal_image(lit: lit, elaboration: e, destination_type: dt, span: span)], + inferred: Present { value: Resolved { node: dt } }, + span: span + )) + LiteralBoundaryRefused { message: m } => + InferResult { typed: plain, diagnostics: [inference_error(message: m, span: span, module_name: scope.module_name)] } + } + + ExprElaboratedLiteral { value: _, elaboration: _ } => + ok_infer(texpr: texpr) ExprError { kind: kind, message: message } => let span = texpr.span @@ -6063,14 +6261,15 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu let span = texpr.span let left_expr = binop_left(texpr: texpr) let right_expr = binop_right(texpr: texpr) - let left_result = infer_expr(texpr: left_expr, scope: scope, expected: none) + let operands = infer_binop_operands(left_expr: left_expr, right_expr: right_expr, scope: scope) + let left_result = operands.left let left_typed = left_result.typed let left_diags = left_result.diagnostics - let right_result = infer_expr(texpr: right_expr, scope: scope, expected: none) + let right_result = operands.right let right_typed = right_result.typed let right_diags = right_result.diagnostics let binop_info = infer_binop_type_node(op: op, left_type: resolved_type(n: left_typed), source_indices: scope.type_env.source_indices) - let bo_texpr = make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprBinOp { op: op, algebra_field: binop_info.algebra_field }, children: [left_typed, right_typed], inferred: Present { value: Resolved { node: binop_info.result_type } }, span: span) + let bo_texpr = make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprBinOp { op: op, algebra_field: binop_info.algebra_field, operand: operand_declaration_of_type(rt: resolved_type(n: left_typed), scope: scope, fuel: 8) }, children: [left_typed, right_typed], inferred: Present { value: Resolved { node: binop_info.result_type } }, span: span) InferResult { typed: bo_texpr, diagnostics: concat(left_diags, right_diags) diff --git a/src/v1/04_resolve.dag b/src/v1/04_resolve.dag index 0db990a4493..13df5958a4d 100644 --- a/src/v1/04_resolve.dag +++ b/src/v1/04_resolve.dag @@ -19,7 +19,7 @@ import v1.std.core { StringPart, Text, Interpolation, MatchPattern, Wildcard, ExprData, NoExprData, - ExprLiteral, ExprError, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, + ExprLiteral, ExprElaboratedLiteral, ExprError, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, ExprMatch, ExprIf, ExprLet, ExprRecordLit, ExprListLit, ExprBinOp, ExprUnaryOp, ExprLambda, ExprStringInterp, ExprBlock, ExprCast, ExprForEach, ExprIndex, ExprSlice, ExprReturn, @@ -848,6 +848,7 @@ fn resolve_transport_binding(transport: Node, env: TypeEnv, module_name: String) fn resolve_expr_types(texpr: Node, env: TypeEnv, module_name: String) -> ExprResolveResult { match texpr.expr_data { ExprLiteral { value: _ } => ExprResolveResult { expr: texpr, diagnostics: [] } + ExprElaboratedLiteral { value: _, elaboration: _ } => ExprResolveResult { expr: texpr, diagnostics: [] } ExprError { kind: kind, message: message } => ExprResolveResult { expr: make_expr_error_node(occurrence_identity: OccurrenceSynthetic, kind: kind, message: message, span: texpr.span), @@ -966,11 +967,11 @@ fn resolve_expr_types(texpr: Node, env: TypeEnv, module_name: String) -> ExprRes let resolved_children = el_results |> map(r => r.expr) let all_diags = flat_map(el_results, r => r.diagnostics) ExprResolveResult { expr: make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprListLit, children: resolved_children, inferred: texpr.inferred, span: texpr.span), diagnostics: all_diags } - ExprBinOp { op: op, algebra_field: af } => + ExprBinOp { op: op, algebra_field: af, operand: od } => let ch = texpr.children let lr = match ch |> first { Present { value: l } => resolve_expr_types(texpr: l, env: env, module_name: module_name) Absent => ExprResolveResult { expr: texpr, diagnostics: [] } } let rr = match ch |> skip(1) |> first { Present { value: r } => resolve_expr_types(texpr: r, env: env, module_name: module_name) Absent => ExprResolveResult { expr: texpr, diagnostics: [] } } - ExprResolveResult { expr: make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprBinOp { op: op, algebra_field: af }, children: [lr.expr, rr.expr], inferred: texpr.inferred, span: texpr.span), diagnostics: concat(lr.diagnostics, rr.diagnostics) } + ExprResolveResult { expr: make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprBinOp { op: op, algebra_field: af, operand: od }, children: [lr.expr, rr.expr], inferred: texpr.inferred, span: texpr.span), diagnostics: concat(lr.diagnostics, rr.diagnostics) } ExprUnaryOp { op: op } => let r = match texpr.children |> first { Present { value: o } => resolve_expr_types(texpr: o, env: env, module_name: module_name) Absent => ExprResolveResult { expr: texpr, diagnostics: [] } } ExprResolveResult { expr: make_expr_node(occurrence_identity: texpr.occurrence_identity, expr_data: ExprUnaryOp { op: op }, children: [r.expr], inferred: texpr.inferred, span: texpr.span), diagnostics: r.diagnostics } diff --git a/src/v1/05_emit.dag b/src/v1/05_emit.dag index fb1064a17f7..4593c9cd4f2 100644 --- a/src/v1/05_emit.dag +++ b/src/v1/05_emit.dag @@ -8,7 +8,7 @@ import v1.std.core { module_imports, module_items, param_node_name_at, param_node_type_expr, qualified_last_segment, param_node_default_value, NewlineIndex, authored_name_at, empty_intern_table, expr_var_name_at, expr_call_func_at, let_binding_name_at, field_access_field_at, ExprData, - NoExprData, VarBindingKind, ExprLiteral, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, + NoExprData, VarBindingKind, ExprLiteral, ExprElaboratedLiteral, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, ExprMatch, ExprIf, ExprLet, ExprRecordLit, ExprListLit, ExprBinOp, ExprUnaryOp, ExprLambda, ExprStringInterp, ExprBlock, ExprCast, ExprForEach, ExprIndex, ExprSlice, ExprError, ExprReturn, StringPart, Text, Interpolation, TextFile, SourceSpan, UnaryOpKind, NullCoalesce, @@ -1264,6 +1264,7 @@ type ExprCategory fn classify_expr(texpr: Node) -> ExprCategory { match texpr.expr_data { ExprLiteral { value: _ } => ExprCatLeaf + ExprElaboratedLiteral { value: _, elaboration: _ } => ExprCatLeaf ExprError { kind: _, message: _ } => ExprCatLeaf ExprVar { binding_kind: _ } => ExprCatLeaf ExprFieldAccess { summary: _ } => ExprCatCompound @@ -2476,6 +2477,11 @@ fn emit_shared_expr( match texpr.expr_data { ExprLiteral { value: v } => wrap_result(emit_literal(value: v, target: target)) + ExprElaboratedLiteral { value: _, elaboration: _ } => + match texpr.children |> first { + Present { value: image } => recurse(image) + Absent => wrap_result(emit_error_expr(message: "elaborated literal carries no image (v1.compiler.infer unfold_literal_image)", target: target)) + } ExprError { kind: _, message: message } => wrap_result(emit_error_expr(message: message, target: target)) ExprVar { binding_kind: _ } => diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index aec0fcea910..d5634a274f6 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -105,8 +105,10 @@ import v1.compiler.closure_stub_v2_std_integer_rust { closure_stub_v2_std_intege import v1.compiler.closure_stub_v2_std_text_rust { closure_stub_v2_std_text_source } import v1.compiler.coercion { coerce_primitive_type, is_copy, lookup_checkpoint, type_reference_decl_file, - rust_seed_host_numeric_alias, target_callable, rust_lookup_exact_binding + rust_seed_host_numeric_alias, target_callable, rust_lookup_exact_binding, + declaration_realizes_natively_on_rust, is_kernel_minted_file } +import v1.compiler.dag_collect_support { connective_name } import v1.compiler.trait_derive_emit { v1_emit_enum_derives, v1_emit_struct_from_capability_table, v1_emit_enum_supplemental_impls, @@ -129,7 +131,16 @@ import v1.compiler.trait_bound_witness { import std.types { is_container_type, is_kernel_type, container_template_algebra } import std.serialization { CoproductWireContract, VariantEncoding, VariantNaming } -import v1.compiler.infer_env { TypeEnv, TypeBinding, authored_name, lookup_type_by_name, lookup_type_for, GlobalBareLookupState, GlobalBareUniqueBinding, GlobalBareAmbiguousBinding, empty_symbol_index } +import v1.compiler.infer_env { TypeEnv, TypeBinding, authored_name, lookup_type_by_name, lookup_type_for, GlobalBareLookupState, GlobalBareUniqueBinding, GlobalBareAmbiguousBinding, empty_symbol_index, binding_declares_span, type_reference_declaration_ref } +import std.operator_realization { + OperatorRealization, HostOperator, StructuralEquality, StructuralComparison, OperatorRealizationRefused, + OperandRealization, HostNumericOperand, StructuralOperand, OperandIdentityUnavailable, + HostRealizedOperand, KernelMintedType, GenericTypeParameter, HostContainer, UnnamedSynthesizedType, + OperandShapeFacts, OperandDeclaration, + StructuralOrderingBinding, OrderingTest, OrderingIs, OrderingIsNot, + operator_realization_for, operator_realization_refusal_message +} +import gunbc.structural_realization_bindings { structural_ordering_rows } import v1.compiler.infer_types { resolved_type, normalize_access_type_node, for_each_element_type_node, child_type_node, emit_map_has, @@ -674,35 +685,9 @@ fn rust_render_checkpoint_scalar_bare(n: Node, source_indices: Map Bool { - match binding.resolved.ident_span { - Present { value: s } => s.file == sp.file && s.start == sp.start - Absent => false - } -} - -fn type_reference_declaration_ref(n: Node, source_indices: Map, env: TypeEnv) -> DeclarationRef? { - let rt = match n.inferred { - Present { value: Resolved { node: r } } => r - _ => n - } - let decl_name = qualified_last_segment(name: authored_name_at(source_indices: source_indices, node: rt)) - if decl_name == "" { return none } - match rt.ident_span { - Absent => none - Present { value: sp } => - match map_get(env.symbol_index.global_bare, decl_name) { - Present { value: GlobalBareUniqueBinding { module_path: mp, binding: b } } => - if binding_declares_span(binding: b, sp: sp) { Present { value: decl_ref(module_path: mp, decl_name: decl_name) } } else { none } - Present { value: GlobalBareAmbiguousBinding { candidates: cands } } => - match cands |> filter(c => binding_declares_span(binding: c.binding, sp: sp)) |> first { - Present { value: c } => Present { value: decl_ref(module_path: c.module_path, decl_name: decl_name) } - Absent => none - } - Absent => none - } - } -} +// binding_declares_span and type_reference_declaration_ref are RELOCATED to v1.compiler.infer_env +// (XL-0N, adhoc-aec65f93-b00): inference now asks the same exact-identity question at every literal +// boundary, and infer_env is the module both stages already import -- one reader, two consumers. // The four arms of the exact resolver, rendered. Two answer a spelling; two are LOUD in the emitted // bytes -- a declaration bound to a representation with no realization row, and two rows for one @@ -10086,8 +10071,8 @@ fn emit_rust_expr_slice(expr: Node, registry: Map, scope: Infe fn emit_rust_expr_bin_op(expr: Node, registry: Map, scope: InferScope, depth: Int, shared_types: Set, emit_info: EmitGraphInfo) -> String { match expr.expr_data { - ExprBinOp { op: op, algebra_field: algebra } => - emit_typed_bin_op(op: op, algebra_field: algebra, left: binop_left(texpr: expr), right: binop_right(texpr: expr), registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info) + ExprBinOp { op: op, algebra_field: algebra, operand: od } => + emit_typed_bin_op(op: op, algebra_field: algebra, operand: od, left: binop_left(texpr: expr), right: binop_right(texpr: expr), registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info) _ => emit_error_expr(message: "emit_rust_expr_bin_op expected ExprBinOp", target: Rust) } } @@ -12133,7 +12118,8 @@ fn emit_field_value_with_context(field_value: Node, struct_node: Node, outer_typ } else { pe } Absent => pe } - let raw = emit_typed_record_lit(type_name: tn, fields: inner_fields, parent_enum: corrected_parent, resolved_type: resolved_type(n: field_value), registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info) + let nested_rt = expand_type_for_field_access(n: resolved_type(n: field_value), env: scope.type_env, module_name: scope.module_name).resolved + let raw = emit_typed_record_lit(type_name: tn, fields: inner_fields, parent_enum: corrected_parent, resolved_type: nested_rt, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info) let rc_name = match corrected_parent { Present { value: en } => en Absent => variant_name @@ -12502,12 +12488,130 @@ fn rust_zero_value(type_name: String) -> String? { else { none } } -fn emit_typed_bin_op(op: BinOp, algebra_field: AlgebraFieldKind?, left: Node, right: Node, registry: Map, scope: InferScope, depth: Int, shared_types: Set, emit_info: EmitGraphInfo) -> String { +fn emit_typed_bin_op(op: BinOp, algebra_field: AlgebraFieldKind?, operand: OperandDeclaration?, left: Node, right: Node, registry: Map, scope: InferScope, depth: Int, shared_types: Set, emit_info: EmitGraphInfo) -> String { let l_str = emit_typed_expr(texpr: left, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info, fuel: 1024) let r_str = emit_typed_expr(texpr: right, registry: registry, scope: scope, depth: depth, shared_types: shared_types, emit_info: emit_info, fuel: 1024) if is_null_coalesce(op: op) { emit_null_coalesce(l_str: l_str, r_str: r_str, target: Rust) } else { + match binop_operator_realization(op: op, operand: operand, left: left, scope: scope) { + OperatorRealizationRefused { cause: c } => + emit_rust_compile_error_expr(message: operator_realization_refusal_message(cause: c)) + StructuralComparison { declaration: _, binding: b, test: t } => + emit_rust_structural_comparison(l_str: l_str, r_str: r_str, binding: b, test: t) + StructuralEquality { declaration: _ } => + emit_rust_host_bin_op(op: op, algebra_field: algebra_field, left: left, right: right, l_str: l_str, r_str: r_str, scope: scope) + HostOperator => + emit_rust_host_bin_op(op: op, algebra_field: algebra_field, left: left, right: right, l_str: l_str, r_str: r_str, scope: scope) + } + } +} + +// OPERATOR REALIZATION BY EXACT OPERAND STRUCTURE (std.operator_realization). The operand's +// declaration is read by identity (v1.compiler.infer_env type_reference_declaration_ref) and its +// native realization asked of the same authority the type renderer asks (v1.compiler.coercion): +// a host numeric keeps the host token; a structural declaration renders equality structurally +// (the emitted enum derives PartialEq over its own constructors) and an ordering as a call to its +// declared comparison tested against std.algebra Ordering; arithmetic on a structural operand +// refuses, typed and located, instead of emitting a token rustc refuses under E0369 later. +fn rust_operand_realization(operand: Node, scope: InferScope) -> OperandRealization { + rust_operand_realization_of_type(rt: resolved_type(n: operand), scope: scope, fuel: 8) +} + +// AN ALIAS OR REFINEMENT DECLARATION REALIZES AS ITS TARGET. `type NonEmptyStr = String where +// non_empty`, `type Char = Int where unicode_scalar, brand("Char")` and their like are alias items +// (is_type_alias_item: a bare-leaf item whose resolved type is a type-alias return node) whose Rust +// realization IS the right-hand side's -- the type renderer already renders them that way -- so the +// operand decision hops to the right-hand side (resolved_type of the declaration) before judging, +// exactly as the derive lane's alias hop does (v1.compiler.trait_derive_emit +// v1_item_alias_hop_type_exprs). The seed's own semver and unicode modules compare NonEmptyStr and +// add to Char; without the hop those were refused as structural. Fuel bounds an alias chain; a +// chain longer than it is judged at its last declaration. +// A `where`-refined declaration resolves to the parser's refinement wrapper -- a one-child Conj +// carrying the predicate as its type_annotation (v1.compiler.parse try_where_clause), which is what +// the operand's resolved node IS at these sites (measured under regen: Conj, one child, no inferred), +// never an alias item. The type renderer already realizes such a node as its base +// (render_rust_alias_rhs_type hops is_where_refinement_type to the first child), so the operand +// decision hops the same way, resolving the base through the env as where_refinement_chain does. +fn rust_operand_realization_of_type(rt: Node, scope: InferScope, fuel: Int) -> OperandRealization { + let decl_file = type_reference_decl_file(n: rt) + let authored = authored_name_at(source_indices: scope.type_env.source_indices, node: rt) + let rt_is_type_var = match rt.inferred { Present { value: i } => is_type_variable(inferred: i) Absent => false } + if is_kernel_minted_file(file: decl_file) { + HostRealizedOperand { reason: KernelMintedType } + } else if rt_is_type_var { + HostRealizedOperand { reason: GenericTypeParameter } + } else if is_container_type(name: qualified_last_segment(name: authored)) { + HostRealizedOperand { reason: HostContainer } + } else if authored == "" { + HostRealizedOperand { reason: UnnamedSynthesizedType } + } else { + match type_reference_declaration_ref(n: rt, source_indices: scope.type_env.source_indices, env: scope.type_env) { + Absent => OperandIdentityUnavailable { facts: OperandShapeFacts { + authored_name: authored, + connective: connective_name(value: rt.connective), + child_count: rt.children |> count, + resolved: rt.inferred != none, + decl_file: decl_file + } } + Present { value: d } => + if declaration_realizes_natively_on_rust(declaration: d, decl_file: type_reference_decl_file(n: rt)) { + HostNumericOperand + } else { + let decl = match rt.inferred { + Present { value: Resolved { node: r } } => r + _ => rt + } + if fuel > 0 && is_where_refinement_type(ty: rt) { + match rt.children |> first { + Present { value: base } => + let base_resolved = match lookup_type_for(env: scope.type_env, node: base) { + Present { value: r } => r + Absent => base + } + rust_operand_realization_of_type(rt: base_resolved, scope: scope, fuel: fuel - 1) + Absent => StructuralOperand { declaration: d } + } + } else if fuel > 0 && is_type_alias_item(item: decl, source_indices: scope.type_env.source_indices) { + rust_operand_realization_of_type(rt: resolved_type(n: decl), scope: scope, fuel: fuel - 1) + } else { + StructuralOperand { declaration: d } + } + } + } + } +} + + +// The operand's declaration is the one inference stamped on the node (std.operator_realization +// OperandDeclaration); the rt-shape read below is the residue for a node that carries none. +fn binop_operator_realization(op: BinOp, operand: OperandDeclaration?, left: Node, scope: InferScope) -> OperatorRealization { + let realization = match operand { + Present { value: od } => + if declaration_realizes_natively_on_rust(declaration: od.declaration, decl_file: od.decl_file) { + HostNumericOperand + } else { + StructuralOperand { declaration: od.declaration } + } + Absent => rust_operand_realization(operand: left, scope: scope) + } + operator_realization_for(op: op, operand: realization, ordering_rows: structural_ordering_rows) +} + +fn rust_declaration_path(module_path: String, decl_name: String) -> String { + concat("crate::", module_to_filename(name: module_path), "::", emit_ident(name: decl_name, target: Rust)) +} + +fn emit_rust_structural_comparison(l_str: String, r_str: String, binding: StructuralOrderingBinding, test: OrderingTest) -> String { + let call = concat(rust_declaration_path(module_path: binding.compare.module_path as String, decl_name: binding.compare.decl_name as String), "(", l_str, ", ", r_str, ")") + let ordering = concat("crate::", module_to_filename(name: binding.ordering.module_path as String), "::", binding.ordering.decl_name as String) + match test { + OrderingIs { variant: v } => concat("(", call, " == ", ordering, "::", v as String, ")") + OrderingIsNot { variant: v } => concat("(", call, " != ", ordering, "::", v as String, ")") + } +} + +fn emit_rust_host_bin_op(op: BinOp, algebra_field: AlgebraFieldKind?, left: Node, right: Node, l_str: String, r_str: String, scope: InferScope) -> String { let op_str = emit_bin_op_symbol(op: op, target: Rust, algebra_field: algebra_field) if is_string_comparison(op: op, left: left, right: right, source_indices: scope.type_env.source_indices) { let l_optional = is_optional_typed_expr(e: left) @@ -12528,7 +12632,6 @@ fn emit_typed_bin_op(op: BinOp, algebra_field: AlgebraFieldKind?, left: Node, ri concat("(", l_str, " ", op_str, " ", r_str, ")") } } - } } fn is_optional_typed_expr(e: Node) -> Bool { diff --git a/src/v1/coercion.dag b/src/v1/coercion.dag index 214d0fd7bc9..8c2b8a00a4a 100644 --- a/src/v1/coercion.dag +++ b/src/v1/coercion.dag @@ -147,6 +147,13 @@ fn numeric_realization_declaring_modules() -> List { ["dag/std/nat.dag", "dag/std/integer.dag", "` pseudo-file, never a declaration in the corpus. One predicate for the three +// places that read it, so the spelling lives here and not in each consumer. +fn is_kernel_minted_file(file: String) -> Bool { + contains(file, " Bool { if decl_file == "" { false @@ -338,6 +345,19 @@ fn rust_exact_realization_decision(source: DeclarationRef?) -> TypeRealizationDe // carries a verdict in gunbc.rust_source_type_bindings, and a name with no verdict is not a table // row at all (false here means the spelling-keyed arm refuses for it). Consulted by // type_realization_decision ahead of the table so a Migrated name cannot be answered by spelling. +// Whether a DECLARATION realizes natively on the Rust target: the exact binding first +// (gunbc.rust_source_type_bindings), then the spelling-keyed checkpoint under the declaration's own +// identity gate (lookup_checkpoint, which refuses a known structural declaration and honours the +// bare-row verdicts). This is the ONE question std.literal_elaboration and std.operator_realization +// ask of the target (XL-0N): a native declaration takes the kernel literal and the host operator +// directly; anything else is a structural operand. +fn declaration_realizes_natively_on_rust(declaration: DeclarationRef, decl_file: String) -> Bool { + match rust_exact_realization_decision(source: Present { value: declaration }) { + Realized { checkpoint: _ } => true + _ => lookup_checkpoint(target: Rust, dag_name: declaration.decl_name as String, decl_file: decl_file) != none + } +} + fn rust_checkpoint_row_keeps_bare_row(dag_name: String) -> Bool { if dag_name == "" { false } else { diff --git a/src/v1/compile.dag b/src/v1/compile.dag index b892e3152be..792d0631d9c 100644 --- a/src/v1/compile.dag +++ b/src/v1/compile.dag @@ -643,6 +643,8 @@ fn serialize_expr_data(expr_node: Node, source_indices: Map "{\"kind\": \"NoExprData\"}" ExprLiteral { value: value } => concat("{\"kind\": \"ExprLiteral\", \"value\": ", serialize_literal(value: value), "}") + ExprElaboratedLiteral { value: value, elaboration: _ } => + concat("{\"kind\": \"ExprElaboratedLiteral\", \"value\": ", serialize_literal(value: value), "}") ExprError { kind: kind, message: message } => concat( "{\"kind\": \"ExprError\", \"error_kind\": ", json_quote(s: expr_error_kind_name(value: kind)), diff --git a/src/v1/complexity.dag b/src/v1/complexity.dag index bee6c3bd817..0588e869099 100644 --- a/src/v1/complexity.dag +++ b/src/v1/complexity.dag @@ -38,7 +38,7 @@ import std.computation { } import std.syntax { BinOp, LiteralValue } import v1.std.core { - Node, NewlineIndex, ExprData, ExprLiteral, ExprError, ExprVar, ExprFieldAccess, ExprCall, + Node, NewlineIndex, ExprData, ExprLiteral, ExprElaboratedLiteral, ExprError, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, ExprBinOp, ExprUnaryOp, Sub, Div, ExprMatch, ExprIf, ExprLet, ExprRecordLit, ExprBlock, ExprForEach, ExprReturn, ExprLambda, MatchPattern, Bind, VariantPattern, field_init_node_name_at, field_init_node_value, arg_name_at, arg_value, arm_body, arm_guard, @@ -4143,6 +4143,17 @@ fn cost_of_expr(texpr: Node, func_index: Map, scc_index: Map< table: table } + ExprElaboratedLiteral { value: _, elaboration: _ } => + SummaryResult { + summary: ComplexitySummary { + work: CostConst { value: 1 }, + span: CostConst { value: 1 }, + output_size: empty_map(), + certainty: Proven + }, + table: table + } + ExprError { kind: _, message: _ } => SummaryResult { summary: ComplexitySummary { diff --git a/src/v1/dag_collect_support.dag b/src/v1/dag_collect_support.dag index ffcac39d682..a47275cec2a 100644 --- a/src/v1/dag_collect_support.dag +++ b/src/v1/dag_collect_support.dag @@ -3,7 +3,7 @@ module v1.compiler.dag_collect_support import v1.std.core { Node, InferredNode, Resolved, CompilerError, TypeVariable, - ExprData, + ExprData, ExprElaboratedLiteral, Connective, NoConnective, Arrow, MatchPattern, Bind, LitPattern, VariantPattern, Wildcard, SourceSpan, ErrorNode, make_error_node, InternalError @@ -55,6 +55,7 @@ fn expr_data_variant(data: ExprData) -> String { match data { NoExprData => "NoExprData" ExprLiteral { value: _ } => "ExprLiteral" + ExprElaboratedLiteral { value: _, elaboration: _ } => "ExprElaboratedLiteral" ExprError { kind: _, message: _ } => "ExprError" ExprVar { binding_kind: _ } => "ExprVar" ExprFieldAccess { summary: _ } => "ExprFieldAccess" diff --git a/src/v1/ownership.dag b/src/v1/ownership.dag index 22ff1662a46..8dec0b7ad43 100644 --- a/src/v1/ownership.dag +++ b/src/v1/ownership.dag @@ -3,7 +3,7 @@ module v1.compiler.ownership import v1.std.core { Node, ExprData, NoExprData, ExprError, - ExprLiteral, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, + ExprLiteral, ExprElaboratedLiteral, ExprVar, ExprFieldAccess, ExprCall, ExprMethodCall, ExprMatch, ExprIf, ExprLet, ExprBlock, ExprReturn, ExprLambda, ExprForEach, ExprRecordLit, VarBindingKind, LocalValueBinding, FunctionValueBinding, @@ -169,6 +169,7 @@ fn walk_expr(accum: UsageAccum, texpr: Node, in_tail: Bool, si: Map accum + ExprElaboratedLiteral { value: _, elaboration: _ } => accum ExprFieldAccess => let base_node = field_access_base(texpr: texpr) @@ -375,6 +376,7 @@ fn collect_callable_refs(texpr: Node, si: Map) -> Set empty_set() } ExprLiteral { value: _ } => empty_set() + ExprElaboratedLiteral { value: _, elaboration: _ } => empty_set() ExprFieldAccess => collect_callable_refs(texpr: field_access_base(texpr: texpr), si: si) ExprCall => diff --git a/src/v1/stage0/src/emitted_population.rs b/src/v1/stage0/src/emitted_population.rs index 3bc691f945f..c7e149db479 100644 --- a/src/v1/stage0/src/emitted_population.rs +++ b/src/v1/stage0/src/emitted_population.rs @@ -38,6 +38,7 @@ // src/gunbc_stage0_emitted_population_manifest.rs // src/gunbc_stage0_executable_assembly_generated.rs // src/gunbc_stage0_partition_package_graph.rs +// src/gunbc_structural_realization_bindings.rs // src/lib.rs // src/main.rs // src/std_algebra.rs @@ -59,6 +60,7 @@ // src/std_interface_summary.rs // src/std_keyed_roster.rs // src/std_keyed_row.rs +// src/std_literal_elaboration.rs // src/std_logic.rs // src/std_machine_constraints.rs // src/std_magnitude.rs @@ -69,6 +71,7 @@ // src/std_occurrence_binding_candidates.rs // src/std_occurrence_binding_resolve.rs // src/std_occurrence_identity.rs +// src/std_operator_realization.rs // src/std_pareto.rs // src/std_primitive_projection.rs // src/std_process_termination.rs diff --git a/src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs b/src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs index 20afea08f33..4dd672c7c2e 100644 --- a/src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs +++ b/src/v1/stage0/src/gunbc_stage0_crate_partition_generated.rs @@ -54,7 +54,7 @@ pub fn generated_partition_crate_rows() -> Rc package_name: "v1-stage0-std-core".to_string(), crate_dir: "src/v1/stage0_std_core".to_string(), kind: GeneratedPartitionCrateKind::GeneratedLayeredCoreCrate, - modules: Rc::new(vec!["std_content_hash".to_string(), "std_coercion".to_string(), "extdeps_currency_currency".to_string(), "std_decl_ref".to_string(), "std_keyed_row".to_string(), "std_keyed_roster".to_string(), "std_roster_frontier".to_string(), "std_dissolution".to_string(), "std_disposition".to_string(), "std_error_primitives".to_string(), "std_emit_model".to_string(), "std_magnitude".to_string(), "std_measure".to_string(), "std_types".to_string(), "std_unicode_types".to_string(), "std_algebra".to_string(), "std_nat".to_string(), "std_node".to_string(), "std_syntax".to_string(), "std_computation".to_string(), "std_termination".to_string(), "std_checked_arithmetic".to_string(), "std_induction".to_string(), "std_graph".to_string(), "extdeps_uri".to_string(), "extdeps_external_authority".to_string(), "std_process_termination".to_string(), "extdeps_container_oci_digest".to_string(), "extdeps_units_dimensionless".to_string(), "extdeps_units_iec_80000_13".to_string(), "extdeps_units_iso8601".to_string(), "extdeps_units_iso_80000_3".to_string(), "std_occurrence_identity".to_string(), "std_source_annotation".to_string(), "std_target_representation".to_string(), "v1_std_core".to_string()]), + modules: Rc::new(vec!["std_content_hash".to_string(), "std_coercion".to_string(), "extdeps_currency_currency".to_string(), "std_decl_ref".to_string(), "std_keyed_row".to_string(), "std_keyed_roster".to_string(), "std_roster_frontier".to_string(), "std_dissolution".to_string(), "std_disposition".to_string(), "std_error_primitives".to_string(), "std_emit_model".to_string(), "std_magnitude".to_string(), "std_measure".to_string(), "std_types".to_string(), "std_unicode_types".to_string(), "std_algebra".to_string(), "std_nat".to_string(), "std_node".to_string(), "std_syntax".to_string(), "std_computation".to_string(), "std_termination".to_string(), "std_checked_arithmetic".to_string(), "std_induction".to_string(), "std_graph".to_string(), "extdeps_uri".to_string(), "extdeps_external_authority".to_string(), "std_process_termination".to_string(), "extdeps_container_oci_digest".to_string(), "extdeps_units_dimensionless".to_string(), "extdeps_units_iec_80000_13".to_string(), "extdeps_units_iso8601".to_string(), "extdeps_units_iso_80000_3".to_string(), "std_occurrence_identity".to_string(), "std_source_annotation".to_string(), "std_target_representation".to_string(), "std_literal_elaboration".to_string(), "std_operator_realization".to_string(), "v1_std_core".to_string()]), reexport_packages: Rc::new(vec!["v1-stage0-runtime".to_string()]), carries_non_empty_wrappers: false, }), Rc::new(GeneratedPartitionCrateRow { @@ -82,7 +82,7 @@ pub fn generated_partition_crate_rows() -> Rc package_name: "v1-stage0-v1-infer".to_string(), crate_dir: "src/v1/stage0_v1_infer".to_string(), kind: GeneratedPartitionCrateKind::GeneratedLayeredCoreCrate, - modules: Rc::new(vec!["gunbc_rust_source_type_bindings".to_string(), "v1_compiler_coercion".to_string(), "v1_compiler_infer_emit_info".to_string(), "v1_compiler_infer_env".to_string(), "v1_compiler_infer_items".to_string(), "v1_compiler_infer_occurrence_binding".to_string(), "v1_compiler_infer_service".to_string(), "v1_compiler_infer_sigs".to_string(), "v1_compiler_infer_types".to_string(), "v1_compiler_type_head_exposure".to_string()]), + modules: Rc::new(vec!["gunbc_rust_source_type_bindings".to_string(), "gunbc_structural_realization_bindings".to_string(), "v1_compiler_coercion".to_string(), "v1_compiler_infer_emit_info".to_string(), "v1_compiler_infer_env".to_string(), "v1_compiler_infer_items".to_string(), "v1_compiler_infer_occurrence_binding".to_string(), "v1_compiler_infer_service".to_string(), "v1_compiler_infer_sigs".to_string(), "v1_compiler_infer_types".to_string(), "v1_compiler_type_head_exposure".to_string()]), reexport_packages: Rc::new(vec!["v1-stage0-runtime".to_string(), "v1-stage0-std-core".to_string(), "v1-stage0-std-surface".to_string(), "v1-stage0-extdeps-languages".to_string(), "v1-stage0-v1-artifact".to_string()]), carries_non_empty_wrappers: false, }), Rc::new(GeneratedPartitionCrateRow { diff --git a/src/v1/stage0/src/gunbc_structural_realization_bindings.rs b/src/v1/stage0/src/gunbc_structural_realization_bindings.rs new file mode 100644 index 00000000000..fd3bbc59e82 --- /dev/null +++ b/src/v1/stage0/src/gunbc_structural_realization_bindings.rs @@ -0,0 +1,89 @@ +// Generated by v1 compiler -- do not edit. +// Source module: gunbc.structural_realization_bindings + +pub use crate::std_decl_ref::decl_ref; +pub use crate::std_decl_ref::DeclarationRef; +use crate::std_literal_elaboration::LiteralSourceKind::{KernelBoolLiteral, KernelIntLiteral}; +use crate::std_literal_elaboration::LiteralUnfolding::{BooleanUnfold, PeanoUnfold}; +pub use crate::std_literal_elaboration::{ + LiteralHomomorphism, LiteralSourceKind, LiteralUnfolding, +}; +pub use crate::std_operator_realization::StructuralOrderingBinding; +use crate::std_types::Bool::*; +pub use crate::std_types::{Bool, List, NonEmptyStr}; +use crate::v1_rt; +use crate::v1_rt::{VecCompat, VecJoin}; +use crate::NonEmptyBTreeSet; +use crate::NonEmptyVec; +use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; +use std::rc::Rc; + +pub fn peano_literal_homomorphism( + module_path: String, + nat: String, + zero: String, + succ: String, + prev_field: String, +) -> Rc { + Rc::new(LiteralHomomorphism { + source_kind: LiteralSourceKind::KernelIntLiteral, + destination: crate::std_decl_ref::decl_ref(module_path.clone(), nat.clone()), + producer: Rc::new(LiteralUnfolding::PeanoUnfold { + zero: crate::std_decl_ref::decl_ref(module_path.clone(), zero.clone()), + succ: crate::std_decl_ref::decl_ref(module_path.clone(), succ.clone()), + prev_field: prev_field.clone(), + }), + }) +} + +pub fn boolean_literal_homomorphism( + module_path: String, + bool_decl: String, + true_variant: String, + false_variant: String, +) -> Rc { + Rc::new(LiteralHomomorphism { + source_kind: LiteralSourceKind::KernelBoolLiteral, + destination: crate::std_decl_ref::decl_ref(module_path.clone(), bool_decl.clone()), + producer: Rc::new(LiteralUnfolding::BooleanUnfold { + true_variant: crate::std_decl_ref::decl_ref(module_path.clone(), true_variant.clone()), + false_variant: crate::std_decl_ref::decl_ref( + module_path.clone(), + false_variant.clone(), + ), + }), + }) +} + +pub fn literal_homomorphism_rows() -> Rc>> { + thread_local! { + static CACHED: Rc>> = { + Rc::new(vec![peano_literal_homomorphism("v2.std.nat".to_string(), "Nat".to_string(), "Zero".to_string(), "Succ".to_string(), "prev".to_string()), boolean_literal_homomorphism("v2.std.logic".to_string(), "Bool".to_string(), "True".to_string(), "False".to_string())]) + }; + } + CACHED.with(|c: &Rc>>| c.clone()) +} + +pub fn structural_ordering_binding( + carrier_module: String, + carrier: String, + compare_module: String, + compare: String, + ordering_module: String, + ordering: String, +) -> Rc { + Rc::new(StructuralOrderingBinding { + carrier: crate::std_decl_ref::decl_ref(carrier_module.clone(), carrier.clone()), + compare: crate::std_decl_ref::decl_ref(compare_module.clone(), compare.clone()), + ordering: crate::std_decl_ref::decl_ref(ordering_module.clone(), ordering.clone()), + }) +} + +pub fn structural_ordering_rows() -> Rc>> { + thread_local! { + static CACHED: Rc>> = { + Rc::new(vec![structural_ordering_binding("v2.std.nat".to_string(), "Nat".to_string(), "v2.std.nat".to_string(), "nat_compare".to_string(), "std.algebra".to_string(), "Ordering".to_string())]) + }; + } + CACHED.with(|c: &Rc>>| c.clone()) +} diff --git a/src/v1/stage0/src/lib.rs b/src/v1/stage0/src/lib.rs index dc102fdcb30..728a033d96d 100644 --- a/src/v1/stage0/src/lib.rs +++ b/src/v1/stage0/src/lib.rs @@ -30,13 +30,16 @@ pub mod gunbc_stage0_crate_partition_generated; pub mod gunbc_stage0_emitted_population_manifest; pub mod gunbc_stage0_executable_assembly_generated; pub mod gunbc_stage0_partition_package_graph; +pub mod gunbc_structural_realization_bindings; pub mod std_constructors; pub mod std_integer; +pub mod std_literal_elaboration; pub mod std_logic; pub mod std_machine_constraints; pub mod std_occurrence_binding; pub mod std_occurrence_binding_candidates; pub mod std_occurrence_binding_resolve; +pub mod std_operator_realization; pub mod std_primitive_projection; pub mod std_reference_binding_observation; pub mod std_repair_input_origin; diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index c120b2c5ae2..3bb89e0fb85 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -431,7 +431,28 @@ pub struct TransitionAdmission { /// `gunbc.bmc_firmware_transition`, and the legacy projection no longer binds them at all — so /// the required run on cdbf4611bb reported `0 unadjudicated delta(s), 31 stale admission(s)`. /// Removed by the roster's own rule before the PR merged, so the rows never reached main. -pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[]; +/// XL-0N (`node://adhoc-aec65f93-b00`, gunbc#9719): ONE relocation, rostered by its author under +/// the rule this ledger states -- "a run carrying a real namespace delta still refuses it as +/// UNADJUDICATED until its author adds a row here". The operand's declaration must be read where +/// the type reference's SCOPED env binding is live, which is inference; `v1.compiler.emit_rust` +/// cannot be imported by `v1.compiler.infer` (emission depends on inference, not the reverse), so +/// the identity read `type_reference_declaration_ref` moves to `v1.compiler.infer_env`, where the +/// only other consumer already lives. The move is the whole change to this spelling: same function, +/// same signature, one declaring module -- not a requalification, and no second declaration is left +/// behind. `emit_rust`'s own call site now resolves to the new declarer, which is the delta below. +/// +/// DISSOLVE-ON: this pull request merging. Base and head then both carry the relocation, no run can +/// produce this delta, the row reports stale on every build, and it is removed by that trigger +/// exactly as all six shrinks above were -- a stale row here refuses every unrelated PR. +pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[TransitionAdmission { + label: "type_reference_declaration_ref relocated to v1.compiler.infer_env (XL-0N, gunbc#9719)", + subject: AdmissionSubject::Binding { + module: "v1.compiler.emit_rust", + in_declaration: "rust_exact_reference_spelling", + spelling: "type_reference_declaration_ref", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, +}]; /// The denominators a green must name (DESIGN §5): a run that cannot say what it covered is an /// instrument failure wearing coverage's clothes. diff --git a/src/v1/stage0/src/std_literal_elaboration.rs b/src/v1/stage0/src/std_literal_elaboration.rs new file mode 100644 index 00000000000..a70d6ddc638 --- /dev/null +++ b/src/v1/stage0/src/std_literal_elaboration.rs @@ -0,0 +1,232 @@ +// Generated by v1 compiler -- do not edit. +// Source module: std.literal_elaboration + +use self::LiteralElaborationOutcome::*; +use self::LiteralElaborationRefusal::*; +use self::LiteralHomomorphismLookup::*; +use self::LiteralSourceKind::*; +use self::LiteralUnfolding::*; +pub use crate::std_decl_ref::declaration_ref_eq; +pub use crate::std_decl_ref::DeclarationRef; +pub use crate::std_syntax::LiteralValue; +use crate::std_syntax::LiteralValue::{LitBool, LitFloat, LitInt, LitNull, LitStr, LitSymbol}; +use crate::std_types::Bool::*; +pub use crate::std_types::{Bool, List, NonEmptyStr}; +use crate::v1_rt; +use crate::v1_rt::{VecCompat, VecJoin}; +use crate::NonEmptyBTreeSet; +use crate::NonEmptyVec; +use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; +use std::rc::Rc; + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum LiteralSourceKind { + KernelIntLiteral, + KernelStringLiteral, + KernelFloatLiteral, + KernelBoolLiteral, + KernelSymbolLiteral, + KernelNullLiteral, +} + +pub fn literal_source_kind_of(value: Rc) -> LiteralSourceKind { + match (*value.clone()).clone() { + LiteralValue::LitInt { value: _, .. } => LiteralSourceKind::KernelIntLiteral, + LiteralValue::LitStr { value: _, .. } => LiteralSourceKind::KernelStringLiteral, + LiteralValue::LitFloat { value: _, .. } => LiteralSourceKind::KernelFloatLiteral, + LiteralValue::LitBool { value: _, .. } => LiteralSourceKind::KernelBoolLiteral, + LiteralValue::LitSymbol { value: _, .. } => LiteralSourceKind::KernelSymbolLiteral, + LiteralValue::LitNull => LiteralSourceKind::KernelNullLiteral, + } +} + +pub fn literal_source_kind_label(kind: LiteralSourceKind) -> String { + match kind.clone() { + LiteralSourceKind::KernelIntLiteral => "kernel_int_literal".to_string(), + LiteralSourceKind::KernelStringLiteral => "kernel_string_literal".to_string(), + LiteralSourceKind::KernelFloatLiteral => "kernel_float_literal".to_string(), + LiteralSourceKind::KernelBoolLiteral => "kernel_bool_literal".to_string(), + LiteralSourceKind::KernelSymbolLiteral => "kernel_symbol_literal".to_string(), + LiteralSourceKind::KernelNullLiteral => "kernel_null_literal".to_string(), + } +} + +pub fn literal_source_kind_eq(a: LiteralSourceKind, b: LiteralSourceKind) -> bool { + (literal_source_kind_label(a.clone()) == literal_source_kind_label(b.clone())) +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum LiteralUnfolding { + PeanoUnfold { + zero: Rc, + succ: Rc, + prev_field: NonEmptyStr, + }, + BooleanUnfold { + true_variant: Rc, + false_variant: Rc, + }, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct LiteralHomomorphism { + pub source_kind: LiteralSourceKind, + pub destination: Rc, + pub producer: Rc, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum LiteralHomomorphismLookup { + LiteralHomomorphismFound { row: Rc }, + LiteralHomomorphismAbsent, + LiteralHomomorphismAmbiguous { row_count: i64 }, +} + +pub fn literal_homomorphism_for( + rows: Rc>>, + source_kind: LiteralSourceKind, + destination: Rc, +) -> Rc { + { + let matching = Rc::new({ + let mut __result = Vec::new(); + for r in rows.iter().cloned() { + if (literal_source_kind_eq(r.source_kind.clone(), source_kind.clone()) + && crate::std_decl_ref::declaration_ref_eq( + r.destination.clone(), + destination.clone(), + )) + { + __result.push(r); + } + } + __result + }); + let n = (matching.clone().len() as i64); + if (n.clone() == 0) { + Rc::new(LiteralHomomorphismLookup::LiteralHomomorphismAbsent) + } else { + if (n.clone() == 1) { + match matching.clone().first().cloned() { + Some(row) => Rc::new(LiteralHomomorphismLookup::LiteralHomomorphismFound { + row: row.clone(), + }), + None => Rc::new(LiteralHomomorphismLookup::LiteralHomomorphismAbsent), + } + } else { + Rc::new(LiteralHomomorphismLookup::LiteralHomomorphismAmbiguous { + row_count: n.clone(), + }) + } + } + } +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum LiteralElaborationRefusal { + HomomorphismDuplicated { + source_kind: LiteralSourceKind, + destination: Rc, + row_count: i64, + }, +} +impl LiteralElaborationRefusal { + pub fn source_kind(&self) -> LiteralSourceKind { + match self { + LiteralElaborationRefusal::HomomorphismDuplicated { + source_kind: __val, .. + } => __val.clone(), + } + } + pub fn destination(&self) -> Rc { + match self { + LiteralElaborationRefusal::HomomorphismDuplicated { + destination: __val, .. + } => __val.clone(), + } + } + pub fn row_count(&self) -> i64 { + match self { + LiteralElaborationRefusal::HomomorphismDuplicated { + row_count: __val, .. + } => __val.clone(), + } + } +} + +pub fn literal_elaboration_refusal_message(cause: Rc) -> String { + match (*cause.clone()).clone() { + LiteralElaborationRefusal::HomomorphismDuplicated { source_kind: k, destination: d, row_count: n, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("literal elaboration: ".to_string(), literal_source_kind_label(k.clone())), " into ".to_string()), d.module_path.clone()), ".".to_string()), d.decl_name.clone()), " has more than one declared homomorphism (gunbc.structural_realization_bindings authoring defect)".to_string()), +} +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum LiteralElaborationOutcome { + DirectLiteral, + ViaHomomorphism { + homomorphism: Rc, + }, + LiteralElaborationRefused { + cause: Rc, + }, +} + +pub fn elaborate_literal_at( + rows: Rc>>, + source_kind: LiteralSourceKind, + destination: Rc, + destination_realizes_natively: bool, +) -> Rc { + if destination_realizes_natively.clone() { + Rc::new(LiteralElaborationOutcome::DirectLiteral) + } else { + match (*literal_homomorphism_for(rows.clone(), source_kind.clone(), destination.clone())) + .clone() + { + LiteralHomomorphismLookup::LiteralHomomorphismFound { row: row, .. } => { + Rc::new(LiteralElaborationOutcome::ViaHomomorphism { + homomorphism: row.clone(), + }) + } + LiteralHomomorphismLookup::LiteralHomomorphismAbsent => { + Rc::new(LiteralElaborationOutcome::DirectLiteral) + } + LiteralHomomorphismLookup::LiteralHomomorphismAmbiguous { row_count: n, .. } => { + Rc::new(LiteralElaborationOutcome::LiteralElaborationRefused { + cause: Rc::new(LiteralElaborationRefusal::HomomorphismDuplicated { + source_kind: source_kind.clone(), + destination: destination.clone(), + row_count: n.clone(), + }), + }) + } + } + } +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct LiteralElaboration { + pub source_kind: LiteralSourceKind, + pub destination: Rc, + pub homomorphism: Rc, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelIntLiteral; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelStringLiteral; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelFloatLiteral; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelBoolLiteral; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelSymbolLiteral; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelNullLiteral; diff --git a/src/v1/stage0/src/std_operator_realization.rs b/src/v1/stage0/src/std_operator_realization.rs new file mode 100644 index 00000000000..5a63ee3f5af --- /dev/null +++ b/src/v1/stage0/src/std_operator_realization.rs @@ -0,0 +1,369 @@ +// Generated by v1 compiler -- do not edit. +// Source module: std.operator_realization + +use self::HostRealizationReason::*; +use self::OperandRealization::*; +use self::OperatorRealization::*; +use self::OperatorRealizationRefusal::*; +use self::OrderingTest::*; +use self::StructuralOrderingLookup::*; +pub use crate::std_decl_ref::declaration_ref_eq; +pub use crate::std_decl_ref::DeclarationRef; +pub use crate::std_syntax::BinOp; +use crate::std_syntax::BinOp::{ + Add, And, Div, Eq, Ge, Gt, Le, Lt, Mod, Mul, Ne, NullCoalesce, Or, Sub, +}; +use crate::std_types::Bool::*; +pub use crate::std_types::{Bool, List, NonEmptyStr}; +use crate::v1_rt; +use crate::v1_rt::{VecCompat, VecJoin}; +use crate::NonEmptyBTreeSet; +use crate::NonEmptyVec; +use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; +use std::rc::Rc; + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct OperandDeclaration { + pub declaration: Rc, + pub decl_file: String, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum OperandRealization { + HostNumericOperand, + HostRealizedOperand { reason: HostRealizationReason }, + StructuralOperand { declaration: Rc }, + OperandIdentityUnavailable { facts: Rc }, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum HostRealizationReason { + KernelMintedType, + GenericTypeParameter, + HostContainer, + UnnamedSynthesizedType, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct OperandShapeFacts { + pub authored_name: String, + pub connective: String, + pub child_count: i64, + pub resolved: bool, + pub decl_file: String, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct StructuralOrderingBinding { + pub carrier: Rc, + pub compare: Rc, + pub ordering: Rc, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum StructuralOrderingLookup { + StructuralOrderingFound { row: Rc }, + StructuralOrderingAbsent, + StructuralOrderingAmbiguous { row_count: i64 }, +} + +pub fn structural_ordering_for( + rows: Rc>>, + carrier: Rc, +) -> Rc { + { + let matching = Rc::new({ + let mut __result = Vec::new(); + for r in rows.iter().cloned() { + if crate::std_decl_ref::declaration_ref_eq(r.carrier.clone(), carrier.clone()) { + __result.push(r); + } + } + __result + }); + let n = (matching.clone().len() as i64); + if (n.clone() == 0) { + Rc::new(StructuralOrderingLookup::StructuralOrderingAbsent) + } else { + if (n.clone() == 1) { + match matching.clone().first().cloned() { + Some(row) => Rc::new(StructuralOrderingLookup::StructuralOrderingFound { + row: row.clone(), + }), + None => Rc::new(StructuralOrderingLookup::StructuralOrderingAbsent), + } + } else { + Rc::new(StructuralOrderingLookup::StructuralOrderingAmbiguous { + row_count: n.clone(), + }) + } + } + } +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum OrderingTest { + OrderingIs { variant: NonEmptyStr }, + OrderingIsNot { variant: NonEmptyStr }, +} +impl OrderingTest { + pub fn variant(&self) -> NonEmptyStr { + match self { + OrderingTest::OrderingIs { variant: __val, .. } => __val.clone(), + OrderingTest::OrderingIsNot { variant: __val, .. } => __val.clone(), + } + } +} + +pub fn ordering_test_for(op: BinOp) -> Option> { + match op.clone() { + BinOp::Lt => Some(Rc::new(OrderingTest::OrderingIs { + variant: "Less".to_string(), + })), + BinOp::Gt => Some(Rc::new(OrderingTest::OrderingIs { + variant: "Greater".to_string(), + })), + BinOp::Le => Some(Rc::new(OrderingTest::OrderingIsNot { + variant: "Greater".to_string(), + })), + BinOp::Ge => Some(Rc::new(OrderingTest::OrderingIsNot { + variant: "Less".to_string(), + })), + BinOp::Add => std::option::Option::None, + BinOp::Sub => std::option::Option::None, + BinOp::Mul => std::option::Option::None, + BinOp::Div => std::option::Option::None, + BinOp::Mod => std::option::Option::None, + BinOp::Eq => std::option::Option::None, + BinOp::Ne => std::option::Option::None, + BinOp::And => std::option::Option::None, + BinOp::Or => std::option::Option::None, + BinOp::NullCoalesce => std::option::Option::None, + } +} + +pub fn binop_label(op: BinOp) -> String { + match op.clone() { + BinOp::Add => "+".to_string(), + BinOp::Sub => "-".to_string(), + BinOp::Mul => "*".to_string(), + BinOp::Div => "/".to_string(), + BinOp::Mod => "%".to_string(), + BinOp::Eq => "==".to_string(), + BinOp::Ne => "!=".to_string(), + BinOp::Lt => "<".to_string(), + BinOp::Gt => ">".to_string(), + BinOp::Le => "<=".to_string(), + BinOp::Ge => ">=".to_string(), + BinOp::And => "&&".to_string(), + BinOp::Or => "||".to_string(), + BinOp::NullCoalesce => "??".to_string(), + } +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum OperatorRealizationRefusal { + NoStructuralOperationDeclared { + declaration: Rc, + operator: BinOp, + }, + StructuralOrderingDuplicated { + declaration: Rc, + row_count: i64, + }, + OperandIdentityUnavailableAt { + operator: BinOp, + facts: Rc, + }, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum OperatorRealization { + HostOperator, + StructuralEquality { + declaration: Rc, + }, + StructuralComparison { + declaration: Rc, + binding: Rc, + test: Rc, + }, + OperatorRealizationRefused { + cause: Rc, + }, +} + +pub fn operator_realization_refusal_message(cause: Rc) -> String { + match (*cause.clone()).clone() { + OperatorRealizationRefusal::NoStructuralOperationDeclared { declaration: d, operator: o, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("operator realization: host operator `".to_string(), binop_label(o.clone())), "` on structural operand ".to_string()), d.module_path.clone()), ".".to_string()), d.decl_name.clone()), " -- the declaration has no host realization and declares no operation for this operator; spell the operation as a call to the declared structural operation".to_string()), + OperatorRealizationRefusal::StructuralOrderingDuplicated { declaration: d, row_count: n, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("operator realization: structural ordering for ".to_string(), d.module_path.clone()), ".".to_string()), d.decl_name.clone()), " has more than one declared comparison (gunbc.structural_realization_bindings authoring defect)".to_string()), + OperatorRealizationRefusal::OperandIdentityUnavailableAt { operator: o, facts: f, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("operator realization: host operator `".to_string(), binop_label(o.clone())), "` on an operand whose declaration could not be read".to_string()), " (authored `".to_string()), f.authored_name.clone()), "`, connective ".to_string()), f.connective.clone()), ", children ".to_string()), (f.child_count.clone()).to_string()), ", resolved ".to_string()), if f.resolved.clone() { + "yes".to_string() + } else { + "no".to_string() + }), ", decl_file `".to_string()), f.decl_file.clone()), "`)".to_string()), +} +} + +pub fn operator_realization_for( + op: BinOp, + operand: Rc, + ordering_rows: Rc>>, +) -> Rc { + match (*operand.clone()).clone() { + OperandRealization::HostNumericOperand => Rc::new(OperatorRealization::HostOperator), + OperandRealization::HostRealizedOperand { reason: _, .. } => { + Rc::new(OperatorRealization::HostOperator) + } + OperandRealization::OperandIdentityUnavailable { facts: f, .. } => match op.clone() { + BinOp::Eq => Rc::new(OperatorRealization::HostOperator), + BinOp::Ne => Rc::new(OperatorRealization::HostOperator), + BinOp::And => Rc::new(OperatorRealization::HostOperator), + BinOp::Or => Rc::new(OperatorRealization::HostOperator), + BinOp::NullCoalesce => Rc::new(OperatorRealization::HostOperator), + BinOp::Lt => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Gt => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Le => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Ge => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Add => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Sub => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Mul => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Div => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + BinOp::Mod => Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::OperandIdentityUnavailableAt { + operator: op.clone(), + facts: f.clone(), + }), + }), + }, + OperandRealization::StructuralOperand { declaration: d, .. } => match op.clone() { + BinOp::Eq => Rc::new(OperatorRealization::StructuralEquality { + declaration: d.clone(), + }), + BinOp::Ne => Rc::new(OperatorRealization::StructuralEquality { + declaration: d.clone(), + }), + BinOp::Lt => { + structural_ordering_realization(op.clone(), d.clone(), ordering_rows.clone()) + } + BinOp::Gt => { + structural_ordering_realization(op.clone(), d.clone(), ordering_rows.clone()) + } + BinOp::Le => { + structural_ordering_realization(op.clone(), d.clone(), ordering_rows.clone()) + } + BinOp::Ge => { + structural_ordering_realization(op.clone(), d.clone(), ordering_rows.clone()) + } + BinOp::And => Rc::new(OperatorRealization::HostOperator), + BinOp::Or => Rc::new(OperatorRealization::HostOperator), + BinOp::NullCoalesce => Rc::new(OperatorRealization::HostOperator), + BinOp::Add => structural_arithmetic_refusal(op.clone(), d.clone()), + BinOp::Sub => structural_arithmetic_refusal(op.clone(), d.clone()), + BinOp::Mul => structural_arithmetic_refusal(op.clone(), d.clone()), + BinOp::Div => structural_arithmetic_refusal(op.clone(), d.clone()), + BinOp::Mod => structural_arithmetic_refusal(op.clone(), d.clone()), + }, + } +} + +pub fn structural_arithmetic_refusal( + op: BinOp, + declaration: Rc, +) -> Rc { + Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::NoStructuralOperationDeclared { + declaration: declaration.clone(), + operator: op.clone(), + }), + }) +} + +pub fn structural_ordering_realization( + op: BinOp, + declaration: Rc, + ordering_rows: Rc>>, +) -> Rc { + match ordering_test_for(op.clone()) { + None => structural_arithmetic_refusal(op.clone(), declaration.clone()), + Some(test) => { + match (*structural_ordering_for(ordering_rows.clone(), declaration.clone())).clone() { + StructuralOrderingLookup::StructuralOrderingFound { row: row, .. } => { + Rc::new(OperatorRealization::StructuralComparison { + declaration: declaration.clone(), + binding: row.clone(), + test: test.clone(), + }) + } + StructuralOrderingLookup::StructuralOrderingAbsent => { + structural_arithmetic_refusal(op.clone(), declaration.clone()) + } + StructuralOrderingLookup::StructuralOrderingAmbiguous { row_count: n, .. } => { + Rc::new(OperatorRealization::OperatorRealizationRefused { + cause: Rc::new(OperatorRealizationRefusal::StructuralOrderingDuplicated { + declaration: declaration.clone(), + row_count: n.clone(), + }), + }) + } + } + } + } +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct KernelMintedType; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct GenericTypeParameter; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct HostContainer; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UnnamedSynthesizedType; diff --git a/src/v1/stage0/src/v1_compiler_coercion.rs b/src/v1/stage0/src/v1_compiler_coercion.rs index 42e2fbd0656..2812011e38b 100644 --- a/src/v1/stage0/src/v1_compiler_coercion.rs +++ b/src/v1/stage0/src/v1_compiler_coercion.rs @@ -225,6 +225,10 @@ pub fn numeric_realization_declaring_modules() -> Rc> { ]) } +pub fn is_kernel_minted_file(file: String) -> bool { + v1_rt::contains(file.clone(), " bool { if (decl_file.clone() == "".to_string()) { false @@ -372,6 +376,22 @@ pub fn rust_exact_realization_decision( } } +pub fn declaration_realizes_natively_on_rust( + declaration: Rc, + decl_file: String, +) -> bool { + match (*rust_exact_realization_decision(Some(declaration.clone()))).clone() { + TypeRealizationDecision::Realized { checkpoint: _, .. } => true, + _ => { + (lookup_checkpoint( + RenderTarget::Rust, + declaration.decl_name.clone(), + decl_file.clone(), + ) != std::option::Option::None) + } + } +} + pub fn rust_checkpoint_row_keeps_bare_row(dag_name: String) -> bool { if (dag_name.clone() == "".to_string()) { false diff --git a/src/v1/stage0/src/v1_compiler_compile.rs b/src/v1/stage0/src/v1_compiler_compile.rs index fba5df214e9..925b535ed71 100644 --- a/src/v1/stage0/src/v1_compiler_compile.rs +++ b/src/v1/stage0/src/v1_compiler_compile.rs @@ -1385,6 +1385,13 @@ pub fn serialize_expr_data( ), "}".to_string(), ), + ExprData::ExprElaboratedLiteral { value, .. } => v1_rt::concat( + v1_rt::concat( + "{\"kind\": \"ExprElaboratedLiteral\", \"value\": ".to_string(), + serialize_literal(value.clone()), + ), + "}".to_string(), + ), ExprData::ExprError { kind, message, .. } => v1_rt::concat( v1_rt::concat( v1_rt::concat( diff --git a/src/v1/stage0/src/v1_compiler_complexity.rs b/src/v1/stage0/src/v1_compiler_complexity.rs index d5740fb0359..abb4f925579 100644 --- a/src/v1/stage0/src/v1_compiler_complexity.rs +++ b/src/v1/stage0/src/v1_compiler_complexity.rs @@ -74,9 +74,9 @@ pub use crate::v1_compiler_parse::{ParserCallIdentity, ParserResultWitness}; use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; use crate::v1_std_core::ExprData::{ - ExprBinOp, ExprBlock, ExprCall, ExprError, ExprFieldAccess, ExprForEach, ExprIf, ExprLambda, - ExprLet, ExprLiteral, ExprMatch, ExprMethodCall, ExprRecordLit, ExprReturn, ExprUnaryOp, - ExprVar, + ExprBinOp, ExprBlock, ExprCall, ExprElaboratedLiteral, ExprError, ExprFieldAccess, ExprForEach, + ExprIf, ExprLambda, ExprLet, ExprLiteral, ExprMatch, ExprMethodCall, ExprRecordLit, ExprReturn, + ExprUnaryOp, ExprVar, }; use crate::v1_std_core::MatchPattern::{Bind, VariantPattern}; use crate::v1_std_core::MethodSemantics::{ @@ -9143,6 +9143,16 @@ pub fn cost_of_expr( }), table: table.clone(), }), + ExprData::ExprElaboratedLiteral { .. } => Rc::new(SummaryResult { + summary: Rc::new(ComplexitySummary { + work: Rc::new(CostExpr::CostConst { value: 1 }), + span: Rc::new(CostExpr::CostConst { value: 1 }), + output_size: v1_rt::rc_empty_map::>(), + certainty: Certainty::Proven, + peak_space: None, + }), + table: table.clone(), + }), ExprData::ExprError { .. } => Rc::new(SummaryResult { summary: Rc::new(ComplexitySummary { work: Rc::new(CostExpr::CostConst { value: 0 }), diff --git a/src/v1/stage0/src/v1_compiler_dag_collect_support.rs b/src/v1/stage0/src/v1_compiler_dag_collect_support.rs index db0508ba939..117d2079769 100644 --- a/src/v1/stage0/src/v1_compiler_dag_collect_support.rs +++ b/src/v1/stage0/src/v1_compiler_dag_collect_support.rs @@ -10,7 +10,7 @@ use crate::v1_rt::{VecCompat, VecJoin}; pub use crate::v1_std_core::make_error_node; use crate::v1_std_core::CompilerDiagnostic::InternalError; use crate::v1_std_core::Connective::{Arrow, NoConnective}; -use crate::v1_std_core::ExprData::*; +use crate::v1_std_core::ExprData::ExprElaboratedLiteral; use crate::v1_std_core::InferredNode::{CompilerError, Resolved, TypeVariable}; use crate::v1_std_core::MatchPattern::{Bind, LitPattern, VariantPattern, Wildcard}; pub use crate::v1_std_core::{ @@ -102,6 +102,7 @@ pub fn expr_data_variant(data: Rc) -> String { match (*data.clone()).clone() { ExprData::NoExprData => "NoExprData".to_string(), ExprData::ExprLiteral { value: _, .. } => "ExprLiteral".to_string(), + ExprData::ExprElaboratedLiteral { .. } => "ExprElaboratedLiteral".to_string(), ExprData::ExprError { .. } => "ExprError".to_string(), ExprData::ExprVar { binding_kind: _, .. diff --git a/src/v1/stage0/src/v1_compiler_emit.rs b/src/v1/stage0/src/v1_compiler_emit.rs index 6ee38dffc00..7da56f5fecd 100644 --- a/src/v1/stage0/src/v1_compiler_emit.rs +++ b/src/v1/stage0/src/v1_compiler_emit.rs @@ -94,9 +94,10 @@ use crate::v1_std_core::Cardinality::CardOptional; use crate::v1_std_core::CompilerDiagnostic::TransportEmissionNotModeled; use crate::v1_std_core::Connective::{Arrow, Conj, Disj, NoConnective}; use crate::v1_std_core::ExprData::{ - ExprBinOp, ExprBlock, ExprCall, ExprCast, ExprError, ExprFieldAccess, ExprForEach, ExprIf, - ExprIndex, ExprLambda, ExprLet, ExprListLit, ExprLiteral, ExprMatch, ExprMethodCall, - ExprRecordLit, ExprReturn, ExprSlice, ExprStringInterp, ExprUnaryOp, ExprVar, NoExprData, + ExprBinOp, ExprBlock, ExprCall, ExprCast, ExprElaboratedLiteral, ExprError, ExprFieldAccess, + ExprForEach, ExprIf, ExprIndex, ExprLambda, ExprLet, ExprListLit, ExprLiteral, ExprMatch, + ExprMethodCall, ExprRecordLit, ExprReturn, ExprSlice, ExprStringInterp, ExprUnaryOp, ExprVar, + NoExprData, }; use crate::v1_std_core::FieldAccessStyle::{TupleFirst, TupleSecond}; use crate::v1_std_core::InferredNode::{CompilerError, Resolved, TypeVariable}; @@ -2817,6 +2818,7 @@ pub enum ExprCategory { pub fn classify_expr(texpr: Rc) -> ExprCategory { match (*texpr.expr_data.clone()).clone() { ExprData::ExprLiteral { value: _, .. } => ExprCategory::ExprCatLeaf, + ExprData::ExprElaboratedLiteral { .. } => ExprCategory::ExprCatLeaf, ExprData::ExprError { .. } => ExprCategory::ExprCatLeaf, ExprData::ExprVar { binding_kind: _, .. @@ -5401,6 +5403,14 @@ pub fn emit_shared_expr( ExprData::ExprLiteral { value: v, .. } => { wrap_result(emit_literal(v.clone(), target.clone())) } + ExprData::ExprElaboratedLiteral { .. } => match texpr.children.clone().first().cloned() { + Some(image) => recurse(image.clone()), + None => wrap_result(emit_error_expr( + "elaborated literal carries no image (v1.compiler.infer unfold_literal_image)" + .to_string(), + target.clone(), + )), + }, ExprData::ExprError { message, .. } => { wrap_result(emit_error_expr(message.clone(), target.clone())) } diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index 4271781effe..c160e048e53 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -39,6 +39,7 @@ pub use crate::gunbc_stage0_emitted_population_manifest::{ }; pub use crate::gunbc_stage0_executable_assembly_generated::generated_host_shell_partition_dependencies; pub use crate::gunbc_stage0_partition_package_graph::stage0_partition_row_is_module_bearing_package; +pub use crate::gunbc_structural_realization_bindings::structural_ordering_rows; pub use crate::std_algebra::trim; pub use crate::std_coercion::TypeCheckpoint; pub use crate::std_content_hash::Fnv1a64Structural; @@ -50,6 +51,23 @@ pub use crate::std_measure::millisecond_count; pub use crate::std_nat::Nat; pub use crate::std_occurrence_identity::NodeOccurrenceIdentity; use crate::std_occurrence_identity::NodeOccurrenceIdentity::OccurrenceSynthetic; +use crate::std_operator_realization::HostRealizationReason::{ + GenericTypeParameter, HostContainer, KernelMintedType, UnnamedSynthesizedType, +}; +use crate::std_operator_realization::OperandRealization::{ + HostNumericOperand, HostRealizedOperand, OperandIdentityUnavailable, StructuralOperand, +}; +use crate::std_operator_realization::OperatorRealization::{ + HostOperator, OperatorRealizationRefused, StructuralComparison, StructuralEquality, +}; +use crate::std_operator_realization::OrderingTest::{OrderingIs, OrderingIsNot}; +pub use crate::std_operator_realization::{ + operator_realization_for, operator_realization_refusal_message, +}; +pub use crate::std_operator_realization::{ + HostRealizationReason, OperandDeclaration, OperandRealization, OperandShapeFacts, + OperatorRealization, OrderingTest, StructuralOrderingBinding, +}; pub use crate::std_primitive_projection::{ primitive_identity_runtime_name, primitive_projection_row_for_declaration, }; @@ -79,10 +97,12 @@ pub use crate::v1_compiler_closure_stub_v2_std_integer_rust::closure_stub_v2_std pub use crate::v1_compiler_closure_stub_v2_std_text_rust::closure_stub_v2_std_text_source; pub use crate::v1_compiler_coercion::decl_identity_file; pub use crate::v1_compiler_coercion::{ - coerce_primitive_type, is_copy, lookup_checkpoint, rust_lookup_exact_binding, - rust_seed_host_numeric_alias, target_callable, type_reference_decl_file, + coerce_primitive_type, declaration_realizes_natively_on_rust, is_copy, is_kernel_minted_file, + lookup_checkpoint, rust_lookup_exact_binding, rust_seed_host_numeric_alias, target_callable, + type_reference_decl_file, }; pub use crate::v1_compiler_compiler_tests_rust::compiler_tests_source; +pub use crate::v1_compiler_dag_collect_support::connective_name; use crate::v1_compiler_emit::BoundOperation::{ BindingRefused, FileBound, LocalBound, RestBound, ShellBound, }; @@ -140,7 +160,8 @@ use crate::v1_compiler_infer_env::GlobalBareLookupState::{ GlobalBareAmbiguousBinding, GlobalBareUniqueBinding, }; pub use crate::v1_compiler_infer_env::{ - authored_name, empty_symbol_index, lookup_type_by_name, lookup_type_for, + authored_name, binding_declares_span, empty_symbol_index, lookup_type_by_name, lookup_type_for, + type_reference_declaration_ref, }; pub use crate::v1_compiler_infer_env::{GlobalBareLookupState, TypeBinding, TypeEnv}; pub use crate::v1_compiler_infer_items::item_kind; @@ -1055,76 +1076,6 @@ pub fn rust_render_checkpoint_scalar_bare( } } -pub fn binding_declares_span(binding: Rc, sp: Rc) -> bool { - match binding.resolved.clone().ident_span.clone() { - Some(s) => ((s.file.clone() == sp.file.clone()) && (s.start.clone() == sp.start.clone())), - None => false, - } -} - -pub fn type_reference_declaration_ref( - n: Rc, - source_indices: Rc>>, - env: Rc, -) -> Option> { - { - let rt = match n.inferred.clone().as_deref().cloned() { - Some(InferredNode::Resolved { node: r, .. }) => r.clone(), - _ => n.clone(), - }; - let decl_name = crate::v1_std_core::qualified_last_segment( - crate::v1_std_core::authored_name_at(source_indices.clone(), rt.clone()), - ); - if (decl_name.clone() == "".to_string()) { - return std::option::Option::None; - } - match rt.ident_span.clone() { - None => std::option::Option::None, - Some(sp) => match v1_rt::map_get( - &env.symbol_index.clone().global_bare.clone(), - decl_name.clone(), - ) - .as_deref() - .cloned() - { - Some(GlobalBareLookupState::GlobalBareUniqueBinding { - module_path: mp, - binding: b, - .. - }) => { - if binding_declares_span(b.clone(), sp.clone()) { - Some(crate::std_decl_ref::decl_ref(mp.clone(), decl_name.clone())) - } else { - std::option::Option::None - } - } - Some(GlobalBareLookupState::GlobalBareAmbiguousBinding { - candidates: cands, - .. - }) => match Rc::new({ - let mut __result = Vec::new(); - for c in cands.iter().cloned() { - if binding_declares_span(c.binding.clone(), sp.clone()) { - __result.push(c); - } - } - __result - }) - .first() - .cloned() - { - Some(c) => Some(crate::std_decl_ref::decl_ref( - c.module_path.clone(), - decl_name.clone(), - )), - None => std::option::Option::None, - }, - None => std::option::Option::None, - }, - } - } -} - pub fn rust_exact_binding_spelling( source: Option>, grounding: bool, @@ -1170,7 +1121,11 @@ pub fn rust_exact_reference_spelling( env: Rc, ) -> Option { rust_exact_binding_spelling( - type_reference_declaration_ref(n.clone(), source_indices.clone(), env.clone()), + crate::v1_compiler_infer_env::type_reference_declaration_ref( + n.clone(), + source_indices.clone(), + env.clone(), + ), false, ) } @@ -22230,10 +22185,12 @@ pub fn emit_rust_expr_bin_op( ExprData::ExprBinOp { op, algebra_field: algebra, + operand: od, .. } => emit_typed_bin_op( op.clone(), algebra.clone(), + od.clone(), crate::v1_std_core::binop_left(expr.clone()), crate::v1_std_core::binop_right(expr.clone()), registry.clone(), @@ -28345,11 +28302,18 @@ pub fn emit_field_value_with_context( } None => pe.clone(), }; + let nested_rt = crate::v1_compiler_infer::expand_type_for_field_access( + crate::v1_compiler_infer_types::resolved_type(field_value.clone()), + scope.type_env.clone(), + scope.module_name.clone(), + ) + .resolved + .clone(); let raw = emit_typed_record_lit( tn.clone(), inner_fields.clone(), corrected_parent.clone(), - crate::v1_compiler_infer_types::resolved_type(field_value.clone()), + nested_rt.clone(), registry.clone(), scope.clone(), depth.clone(), @@ -29547,6 +29511,7 @@ pub fn rust_zero_value(type_name: String) -> Option { pub fn emit_typed_bin_op( op: BinOp, algebra_field: Option, + operand: Option>, left: Rc, right: Rc, registry: Rc>>, @@ -29581,133 +29546,411 @@ pub fn emit_typed_bin_op( RenderTarget::Rust, ) } else { + match (*binop_operator_realization( + op.clone(), + operand.clone(), + left.clone(), + scope.clone(), + )) + .clone() { - let op_str = crate::v1_compiler_emit::emit_bin_op_symbol( + OperatorRealization::OperatorRealizationRefused { cause: c, .. } => { + emit_rust_compile_error_expr( + crate::std_operator_realization::operator_realization_refusal_message( + c.clone(), + ), + ) + } + OperatorRealization::StructuralComparison { + binding: b, + test: t, + .. + } => emit_rust_structural_comparison( + l_str.clone(), + r_str.clone(), + b.clone(), + t.clone(), + ), + OperatorRealization::StructuralEquality { declaration: _, .. } => { + emit_rust_host_bin_op( + op.clone(), + algebra_field.clone(), + left.clone(), + right.clone(), + l_str.clone(), + r_str.clone(), + scope.clone(), + ) + } + OperatorRealization::HostOperator => emit_rust_host_bin_op( op.clone(), - RenderTarget::Rust, algebra_field.clone(), - ); - if is_string_comparison( - op.clone(), left.clone(), right.clone(), - scope.type_env.clone().source_indices.clone(), + l_str.clone(), + r_str.clone(), + scope.clone(), + ), + } + } + } +} + +pub fn rust_operand_realization( + operand: Rc, + scope: Rc, +) -> Rc { + rust_operand_realization_of_type( + crate::v1_compiler_infer_types::resolved_type(operand.clone()), + scope.clone(), + 8, + ) +} + +pub fn rust_operand_realization_of_type( + mut rt: Rc, + mut scope: Rc, + mut fuel: i64, +) -> Rc { + loop { + let decl_file = crate::v1_compiler_coercion::type_reference_decl_file(rt.clone()); + let authored = crate::v1_std_core::authored_name_at( + scope.type_env.clone().source_indices.clone(), + rt.clone(), + ); + let rt_is_type_var = match rt.inferred.clone() { + Some(i) => is_type_variable(i.clone()), + None => false, + }; + if crate::v1_compiler_coercion::is_kernel_minted_file(decl_file.clone()) { + break Rc::new(OperandRealization::HostRealizedOperand { + reason: HostRealizationReason::KernelMintedType, + }); + } else { + if rt_is_type_var.clone() { + break Rc::new(OperandRealization::HostRealizedOperand { + reason: HostRealizationReason::GenericTypeParameter, + }); + } else { + if crate::std_types::is_container_type(crate::v1_std_core::qualified_last_segment( + authored.clone(), + )) { + break Rc::new(OperandRealization::HostRealizedOperand { + reason: HostRealizationReason::HostContainer, + }); + } else { + if (authored.clone() == "".to_string()) { + break Rc::new(OperandRealization::HostRealizedOperand { + reason: HostRealizationReason::UnnamedSynthesizedType, + }); + } else { + match crate::v1_compiler_infer_env::type_reference_declaration_ref(rt.clone(), scope.type_env.clone().source_indices.clone(), scope.type_env.clone()) { + None => { break Rc::new(OperandRealization::OperandIdentityUnavailable { + facts: Rc::new(OperandShapeFacts { + authored_name: authored.clone(), + connective: crate::v1_compiler_dag_collect_support::connective_name(rt.connective.clone()), + child_count: (rt.children.clone().len() as i64), + resolved: (rt.inferred.clone() != std::option::Option::None), + decl_file: decl_file.clone(), +}), +}); }, + Some(d) => { if crate::v1_compiler_coercion::declaration_realizes_natively_on_rust(d.clone(), crate::v1_compiler_coercion::type_reference_decl_file(rt.clone())) { + break Rc::new(OperandRealization::HostNumericOperand); +} else { + let decl = match rt.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { node: r, .. }) => r.clone(), + _ => rt.clone(), +}; +if ((fuel.clone() > 0) && crate::v1_compiler_infer::is_where_refinement_type(rt.clone())) { + match rt.children.clone().first().cloned() { + Some(base) => { let base_resolved = match crate::v1_compiler_infer_env::lookup_type_for(scope.type_env.clone(), base.clone()) { + Some(r) => r.clone(), + None => base.clone(), +}; +{ + let __tco_0 = base_resolved.clone(); +let __tco_1 = (fuel - 1); +rt = __tco_0; +fuel = __tco_1; +continue; +} }, + None => { break Rc::new(OperandRealization::StructuralOperand { + declaration: d.clone(), +}); }, +} +} else { + if ((fuel.clone() > 0) && crate::v1_compiler_emit_core_support::is_type_alias_item(decl.clone(), scope.type_env.clone().source_indices.clone())) { + { + let __tco_0 = crate::v1_compiler_infer_types::resolved_type(decl.clone()); +let __tco_1 = (fuel - 1); +rt = __tco_0; +fuel = __tco_1; +continue; +} +} else { + break Rc::new(OperandRealization::StructuralOperand { + declaration: d.clone(), +}); +} +} +} }, +} + } + } + } + } + } +} + +pub fn binop_operator_realization( + op: BinOp, + operand: Option>, + left: Rc, + scope: Rc, +) -> Rc { + { + let realization = match operand.clone() { + Some(od) => { + if crate::v1_compiler_coercion::declaration_realizes_natively_on_rust( + od.declaration.clone(), + od.decl_file.clone(), ) { + Rc::new(OperandRealization::HostNumericOperand) + } else { + Rc::new(OperandRealization::StructuralOperand { + declaration: od.declaration.clone(), + }) + } + } + None => rust_operand_realization(left.clone(), scope.clone()), + }; + crate::std_operator_realization::operator_realization_for( + op.clone(), + realization.clone(), + structural_ordering_rows(), + ) + } +} + +pub fn rust_declaration_path(module_path: String, decl_name: String) -> String { + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + "crate::".to_string(), + crate::v1_compiler_emit_core_support::module_to_filename(module_path.clone()), + ), + "::".to_string(), + ), + crate::v1_compiler_emit::emit_ident(decl_name.clone(), RenderTarget::Rust), + ) +} + +pub fn emit_rust_structural_comparison( + l_str: String, + r_str: String, + binding: Rc, + test: Rc, +) -> String { + { + let call = v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + rust_declaration_path( + binding.compare.clone().module_path.clone(), + binding.compare.clone().decl_name.clone(), + ), + "(".to_string(), + ), + l_str.clone(), + ), + ", ".to_string(), + ), + r_str.clone(), + ), + ")".to_string(), + ); + let ordering = v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + "crate::".to_string(), + crate::v1_compiler_emit_core_support::module_to_filename( + binding.ordering.clone().module_path.clone(), + ), + ), + "::".to_string(), + ), + binding.ordering.clone().decl_name.clone(), + ); + match (*test.clone()).clone() { + OrderingTest::OrderingIs { variant: v, .. } => v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat("(".to_string(), call.clone()), + " == ".to_string(), + ), + ordering.clone(), + ), + "::".to_string(), + ), + v.clone(), + ), + ")".to_string(), + ), + OrderingTest::OrderingIsNot { variant: v, .. } => v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat("(".to_string(), call.clone()), + " != ".to_string(), + ), + ordering.clone(), + ), + "::".to_string(), + ), + v.clone(), + ), + ")".to_string(), + ), + } + } +} + +pub fn emit_rust_host_bin_op( + op: BinOp, + algebra_field: Option, + left: Rc, + right: Rc, + l_str: String, + r_str: String, + scope: Rc, +) -> String { + { + let op_str = crate::v1_compiler_emit::emit_bin_op_symbol( + op.clone(), + RenderTarget::Rust, + algebra_field.clone(), + ); + if is_string_comparison( + op.clone(), + left.clone(), + right.clone(), + scope.type_env.clone().source_indices.clone(), + ) { + { + let l_optional = is_optional_typed_expr(left.clone()); + let r_optional = is_optional_typed_expr(right.clone()); + if (l_optional.clone() || r_optional.clone()) { { - let l_optional = is_optional_typed_expr(left.clone()); - let r_optional = is_optional_typed_expr(right.clone()); - if (l_optional.clone() || r_optional.clone()) { - { - let l_cmp = if l_optional.clone() { - v1_rt::concat(l_str.clone(), ".as_deref()".to_string()) - } else { - v1_rt::concat( - v1_rt::concat( - "Some(".to_string(), - emit_rust_dag_string_to_host_via_seam(l_str.clone()), - ), - ").as_deref()".to_string(), - ) - }; - let r_cmp = if r_optional.clone() { - v1_rt::concat(r_str.clone(), ".as_deref()".to_string()) - } else { - v1_rt::concat( - v1_rt::concat( - "Some(".to_string(), - emit_rust_dag_string_to_host_via_seam(r_str.clone()), - ), - ").as_deref()".to_string(), - ) - }; + let l_cmp = if l_optional.clone() { + v1_rt::concat(l_str.clone(), ".as_deref()".to_string()) + } else { + v1_rt::concat( + v1_rt::concat( + "Some(".to_string(), + emit_rust_dag_string_to_host_via_seam(l_str.clone()), + ), + ").as_deref()".to_string(), + ) + }; + let r_cmp = if r_optional.clone() { + v1_rt::concat(r_str.clone(), ".as_deref()".to_string()) + } else { + v1_rt::concat( + v1_rt::concat( + "Some(".to_string(), + emit_rust_dag_string_to_host_via_seam(r_str.clone()), + ), + ").as_deref()".to_string(), + ) + }; + v1_rt::concat( + v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat( - v1_rt::concat( - v1_rt::concat("(".to_string(), l_cmp.clone()), - " ".to_string(), - ), - op_str.clone(), - ), + v1_rt::concat("(".to_string(), l_cmp.clone()), " ".to_string(), ), - r_cmp.clone(), + op_str.clone(), ), - ")".to_string(), - ) - } - } else { + " ".to_string(), + ), + r_cmp.clone(), + ), + ")".to_string(), + ) + } + } else { + v1_rt::concat( + v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat( - v1_rt::concat( - "(".to_string(), - emit_rust_dag_string_to_host_via_seam( - l_str.clone(), - ), - ), - " ".to_string(), - ), - op_str.clone(), + "(".to_string(), + emit_rust_dag_string_to_host_via_seam(l_str.clone()), ), " ".to_string(), ), - emit_rust_dag_string_to_host_via_seam(r_str.clone()), + op_str.clone(), ), - ")".to_string(), - ) - } - } - } else { - { - let both_string = (is_string_typed_expr( - left.clone(), - scope.type_env.clone().source_indices.clone(), - ) && is_string_typed_expr( - right.clone(), - scope.type_env.clone().source_indices.clone(), - )); - let is_str_concat = - ((op_str.clone() == "+".to_string()) && both_string.clone()); - if is_str_concat.clone() { + " ".to_string(), + ), + emit_rust_dag_string_to_host_via_seam(r_str.clone()), + ), + ")".to_string(), + ) + } + } + } else { + { + let both_string = (is_string_typed_expr( + left.clone(), + scope.type_env.clone().source_indices.clone(), + ) && is_string_typed_expr( + right.clone(), + scope.type_env.clone().source_indices.clone(), + )); + let is_str_concat = ((op_str.clone() == "+".to_string()) && both_string.clone()); + if is_str_concat.clone() { + v1_rt::concat( + v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat( - v1_rt::concat( - v1_rt::concat("(".to_string(), l_str.clone()), - " ".to_string(), - ), - op_str.clone(), - ), - " &".to_string(), + v1_rt::concat("(".to_string(), l_str.clone()), + " ".to_string(), ), - r_str.clone(), + op_str.clone(), ), - ")".to_string(), - ) - } else { + " &".to_string(), + ), + r_str.clone(), + ), + ")".to_string(), + ) + } else { + v1_rt::concat( + v1_rt::concat( v1_rt::concat( v1_rt::concat( v1_rt::concat( - v1_rt::concat( - v1_rt::concat( - v1_rt::concat("(".to_string(), l_str.clone()), - " ".to_string(), - ), - op_str.clone(), - ), + v1_rt::concat("(".to_string(), l_str.clone()), " ".to_string(), ), - r_str.clone(), + op_str.clone(), ), - ")".to_string(), - ) - } - } + " ".to_string(), + ), + r_str.clone(), + ), + ")".to_string(), + ) } } } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 8eae32c8000..9e245cf80e5 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -7,10 +7,12 @@ use self::DescentSizeExpr::*; use self::InhabitanceRefusalReason::*; use self::InhabitanceUndecidableReason::*; use self::InhabitanceVerdict::*; +use self::LiteralBoundary::*; use self::ServiceConfigFieldJudgment::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, }; +pub use crate::gunbc_structural_realization_bindings::literal_homomorphism_rows; pub use crate::std_algebra::AlgebraFieldTemplate; use crate::std_algebra::CollectionSizeEffect::ShrinkEffect; pub use crate::std_algebra::{CollectionSizeEffect, FreeMonoid}; @@ -23,6 +25,7 @@ pub use crate::std_content_hash::{ content_hash_validate_lower_hex_length, }; pub use crate::std_content_hash::{ContentHash, Fnv1a64Structural}; +pub use crate::std_decl_ref::DeclarationRef; pub use crate::std_dissolution::DissolutionCondition; use crate::std_dissolution::DissolutionCondition::*; pub use crate::std_dissolution::{dissolution_description, unbound_dissolution}; @@ -41,14 +44,25 @@ pub use crate::std_induction::{InductiveField, RecursionShape, SubValueRelation} use crate::std_interface_summary::ExportKind::{ExportData, ExportFn, ExportService, ExportType}; pub use crate::std_interface_summary::{interface_summary_rollup, signature_contract}; pub use crate::std_interface_summary::{ExportEntry, ExportKind, InterfaceSummary}; +use crate::std_literal_elaboration::LiteralElaborationOutcome::{ + DirectLiteral, LiteralElaborationRefused, ViaHomomorphism, +}; +use crate::std_literal_elaboration::LiteralUnfolding::{BooleanUnfold, PeanoUnfold}; +pub use crate::std_literal_elaboration::{ + elaborate_literal_at, literal_elaboration_refusal_message, literal_source_kind_of, +}; +pub use crate::std_literal_elaboration::{ + LiteralElaboration, LiteralElaborationOutcome, LiteralHomomorphism, LiteralUnfolding, +}; pub use crate::std_node::{compiler_inductive_fields, compiler_recursive_types}; pub use crate::std_occurrence_identity::NodeOccurrenceIdentity; use crate::std_occurrence_identity::NodeOccurrenceIdentity::OccurrenceSynthetic; pub use crate::std_occurrence_identity::OccurrenceId; +pub use crate::std_operator_realization::OperandDeclaration; use crate::std_syntax::BinOp::Add; use crate::std_syntax::BinOp::{And, Div, Eq, Ge, Gt, Le, Lt, Mod, Mul, Ne, NullCoalesce, Or, Sub}; -use crate::std_syntax::LiteralValue::LitStr; -use crate::std_syntax::LiteralValue::{LitBool, LitFloat, LitInt, LitNull}; +use crate::std_syntax::LiteralValue::{LitBool, LitInt, LitStr}; +use crate::std_syntax::LiteralValue::{LitFloat, LitNull}; pub use crate::std_syntax::{BinOp, LiteralValue}; pub use crate::std_termination::PositiveDescentAmount; use crate::std_termination::PositiveDescentAmount::OneStep; @@ -86,7 +100,8 @@ pub use crate::v1_compiler_infer_env::{ node_with_inferred, put_inductive_field, put_inductive_field_cross, qualified_all_but_last, qualify_borrowed_inferred, qualify_borrowed_type_names, qualify_decl_reference_positions, str_bindings_from_bindings, symbol_index_insert, symbol_index_insert_decl, - symbol_index_insert_service, symbol_index_lookup, unit_variant_index_shadow_insert, + symbol_index_insert_service, symbol_index_lookup, type_reference_declaration, + type_reference_declaration_ref, unit_variant_index_shadow_insert, }; pub use crate::v1_compiler_infer_env::{ GlobalBareCandidate, GlobalBareLookupState, GuardedTypeEnvCacheMerge, ServiceCensusEntry, @@ -206,9 +221,10 @@ use crate::v1_std_core::CompilerDiagnostic::{ }; use crate::v1_std_core::Connective::{Arrow, Conj, Disj, NoConnective}; use crate::v1_std_core::ExprData::{ - ExprBinOp, ExprBlock, ExprCall, ExprCast, ExprError, ExprFieldAccess, ExprForEach, ExprIf, - ExprIndex, ExprLambda, ExprLet, ExprListLit, ExprLiteral, ExprMatch, ExprMethodCall, - ExprRecordLit, ExprReturn, ExprSlice, ExprStringInterp, ExprUnaryOp, ExprVar, NoExprData, + ExprBinOp, ExprBlock, ExprCall, ExprCast, ExprElaboratedLiteral, ExprError, ExprFieldAccess, + ExprForEach, ExprIf, ExprIndex, ExprLambda, ExprLet, ExprListLit, ExprLiteral, ExprMatch, + ExprMethodCall, ExprRecordLit, ExprReturn, ExprSlice, ExprStringInterp, ExprUnaryOp, ExprVar, + NoExprData, }; use crate::v1_std_core::ExprErrorKind::{ CensusHeadsBodyStripped, InternalExprError, ParseRecoveryError, SemanticExprError, @@ -7672,6 +7688,289 @@ pub fn qualified_value_projection( } } +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum LiteralBoundary { + LiteralBoundaryPlain, + LiteralBoundaryElaborated { + elaboration: Rc, + destination_type: Rc, + }, + LiteralBoundaryRefused { + message: String, + }, +} + +pub fn literal_boundary_elaboration( + lit: Rc, + expected: Option>, + scope: Rc, +) -> Rc { + match expected.clone() { + None => Rc::new(LiteralBoundary::LiteralBoundaryPlain), + Some(exp) => { + if (exp.return_cardinality.clone() == Cardinality::CardOptional) { + Rc::new(LiteralBoundary::LiteralBoundaryPlain) + } else { + match crate::v1_compiler_infer_env::type_reference_declaration_ref( + exp.clone(), + scope.type_env.clone().source_indices.clone(), + scope.type_env.clone(), + ) { + None => Rc::new(LiteralBoundary::LiteralBoundaryPlain), + Some(destination) => { + let kind = + crate::std_literal_elaboration::literal_source_kind_of(lit.clone()); + let natively = crate::v1_compiler_coercion::decl_file_realizes_natively( + crate::v1_compiler_coercion::type_reference_decl_file(exp.clone()), + ); + match (*crate::std_literal_elaboration::elaborate_literal_at(literal_homomorphism_rows(), kind.clone(), destination.clone(), natively.clone())).clone() { + LiteralElaborationOutcome::DirectLiteral => Rc::new(LiteralBoundary::LiteralBoundaryPlain), + LiteralElaborationOutcome::ViaHomomorphism { homomorphism: h, .. } => Rc::new(LiteralBoundary::LiteralBoundaryElaborated { + elaboration: Rc::new(LiteralElaboration { + source_kind: kind.clone(), + destination: destination.clone(), + homomorphism: h.clone(), +}), + destination_type: exp.clone(), +}), + LiteralElaborationOutcome::LiteralElaborationRefused { cause: c, .. } => Rc::new(LiteralBoundary::LiteralBoundaryRefused { + message: crate::std_literal_elaboration::literal_elaboration_refusal_message(c.clone()), +}), +} + } + } + } + } + } +} + +pub fn elaborated_span(name: String) -> Rc { + Rc::new(SourceSpan { + file: "".to_string(), + start: 0, + end: v1_rt::string_length(&name), + }) +} + +pub fn elaborated_expr_node( + name: String, + expr_data: Rc, + children: Rc>>, + destination_type: Rc, + span: Rc, +) -> Rc { + Rc::new(Node { + occurrence_identity: Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), + name: name.clone(), + span: span.clone(), + ident_span: Some(elaborated_span(name.clone())), + children: children.clone(), + connective: Connective::NoConnective, + params: Rc::new(vec![]), + inferred: Some(Rc::new(InferredNode::Resolved { + node: destination_type.clone(), + })), + return_cardinality: Cardinality::Required, + uses: Rc::new(vec![]), + body: std::option::Option::None, + transport: std::option::Option::None, + properties: Rc::new(vec![]), + type_annotation: std::option::Option::None, + is_self_recursive: false, + has_non_tail_self_call: false, + match_pattern: std::option::Option::None, + expr_data: expr_data.clone(), + ident: None, + }) +} + +pub fn unfold_peano_image( + n: i64, + zero: String, + succ: String, + prev_field: String, + parent: String, + destination_type: Rc, + span: Rc, +) -> Rc { + stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || { + if (n.clone() <= 0) { + elaborated_expr_node( + zero.clone(), + Rc::new(ExprData::ExprVar { + binding_kind: Some(Rc::new(VarBindingKind::VariantValueBinding { + parent_enum: parent.clone(), + })), + }), + Rc::new(vec![]), + destination_type.clone(), + span.clone(), + ) + } else { + { + let prev = unfold_peano_image( + (n.clone() - 1), + zero.clone(), + succ.clone(), + prev_field.clone(), + parent.clone(), + destination_type.clone(), + span.clone(), + ); + let field = crate::v1_std_core::make_field_init_node( + Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), + prev_field.clone(), + prev.clone(), + span.clone(), + elaborated_span(prev_field.clone()), + ); + elaborated_expr_node( + succ.clone(), + Rc::new(ExprData::ExprRecordLit { + parent_enum: Some(parent.clone()), + }), + Rc::new(vec![field.clone()]), + destination_type.clone(), + span.clone(), + ) + } + } + }) +} + +pub fn unfold_literal_image( + lit: Rc, + elaboration: Rc, + destination_type: Rc, + span: Rc, +) -> Rc { + match (*elaboration.homomorphism.clone().producer.clone()).clone() { + LiteralUnfolding::PeanoUnfold { zero, succ, prev_field, .. } => match (*lit.clone()).clone() { + LiteralValue::LitInt { value: n, .. } => unfold_peano_image(n.clone(), zero.decl_name.clone(), succ.decl_name.clone(), prev_field.clone(), elaboration.destination.clone().decl_name.clone(), destination_type.clone(), span.clone()), + _ => crate::v1_std_core::make_expr_error_node(Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), ExprErrorKind::InternalExprError, "literal elaboration: a Peano unfolding row was selected for a non-integer literal (gunbc.structural_realization_bindings keys the row on KernelIntLiteral, so this row is malformed)".to_string(), span.clone()), +}, + LiteralUnfolding::BooleanUnfold { true_variant: t, false_variant: f, .. } => match (*lit.clone()).clone() { + LiteralValue::LitBool { value: b, .. } => elaborated_expr_node(if b.clone() { + t.decl_name.clone() + } else { + f.decl_name.clone() + }, Rc::new(ExprData::ExprVar { + binding_kind: Some(Rc::new(VarBindingKind::VariantValueBinding { + parent_enum: elaboration.destination.clone().decl_name.clone(), +})), +}), Rc::new(vec![]), destination_type.clone(), span.clone()), + _ => crate::v1_std_core::make_expr_error_node(Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), ExprErrorKind::InternalExprError, "literal elaboration: a Boolean unfolding row was selected for a non-boolean literal (gunbc.structural_realization_bindings keys the row on KernelBoolLiteral, so this row is malformed)".to_string(), span.clone()), +}, +} +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct BinopOperands { + pub left: Rc, + pub right: Rc, +} + +pub fn operand_declaration_of_type( + mut rt: Rc, + mut scope: Rc, + mut fuel: i64, +) -> Option> { + loop { + if ((fuel.clone() > 0) && is_where_refinement_type(rt.clone())) { + match rt.children.clone().first().cloned() { + Some(base) => { + let base_resolved = match crate::v1_compiler_infer_env::lookup_type_for( + scope.type_env.clone(), + base.clone(), + ) { + Some(r) => r.clone(), + None => base.clone(), + }; + { + let __tco_0 = base_resolved.clone(); + let __tco_1 = (fuel - 1); + rt = __tco_0; + fuel = __tco_1; + continue; + } + } + None => { + break crate::v1_compiler_infer_env::type_reference_declaration( + rt.clone(), + scope.type_env.clone().source_indices.clone(), + scope.type_env.clone(), + ); + } + } + } else { + break crate::v1_compiler_infer_env::type_reference_declaration( + rt.clone(), + scope.type_env.clone().source_indices.clone(), + scope.type_env.clone(), + ); + } + } +} + +pub fn infer_operand_literal( + lit_expr: Rc, + other: Rc, + scope: Rc, +) -> Rc { + { + let other_type = match other.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { node: rt, .. }) => Some(rt.clone()), + _ => std::option::Option::None, + }; + infer_expr_body(lit_expr.clone(), scope.clone(), other_type.clone()) + } +} + +pub fn infer_binop_operands( + left_expr: Rc, + right_expr: Rc, + scope: Rc, +) -> Rc { + { + let left_is_literal = expr_is_any_literal(left_expr.clone()); + let right_is_literal = expr_is_any_literal(right_expr.clone()); + if (right_is_literal.clone() && !left_is_literal.clone()) { + { + let l = infer_expr(left_expr.clone(), scope.clone(), std::option::Option::None); + Rc::new(BinopOperands { + left: l.clone(), + right: infer_operand_literal( + right_expr.clone(), + l.typed.clone(), + scope.clone(), + ), + }) + } + } else { + if (left_is_literal.clone() && !right_is_literal.clone()) { + { + let r = + infer_expr(right_expr.clone(), scope.clone(), std::option::Option::None); + Rc::new(BinopOperands { + left: infer_operand_literal( + left_expr.clone(), + r.typed.clone(), + scope.clone(), + ), + right: r.clone(), + }) + } + } else { + Rc::new(BinopOperands { + left: infer_expr(left_expr.clone(), scope.clone(), std::option::Option::None), + right: infer_expr(right_expr.clone(), scope.clone(), std::option::Option::None), + }) + } + } + } +} + pub fn infer_expr_body( texpr: Rc, scope: Rc, @@ -7680,7 +7979,7 @@ pub fn infer_expr_body( match (*texpr.expr_data.clone()).clone() { ExprData::ExprLiteral { value: lit, .. } => { let span = texpr.span.clone(); - ok_infer(crate::v1_std_core::make_expr_node( + let plain = crate::v1_std_core::make_expr_node( texpr.occurrence_identity.clone(), Rc::new(ExprData::ExprLiteral { value: lit.clone() }), Rc::new(vec![]), @@ -7688,8 +7987,43 @@ pub fn infer_expr_body( node: crate::v1_compiler_infer_types::infer_literal_node(lit.clone()), })), span.clone(), - )) + ); + match (*literal_boundary_elaboration(lit.clone(), expected.clone(), scope.clone())) + .clone() + { + LiteralBoundary::LiteralBoundaryPlain => ok_infer(plain.clone()), + LiteralBoundary::LiteralBoundaryElaborated { + elaboration: e, + destination_type: dt, + .. + } => ok_infer(crate::v1_std_core::make_expr_node( + texpr.occurrence_identity.clone(), + Rc::new(ExprData::ExprElaboratedLiteral { + value: lit.clone(), + elaboration: e.clone(), + }), + Rc::new(vec![unfold_literal_image( + lit.clone(), + e.clone(), + dt.clone(), + span.clone(), + )]), + Some(Rc::new(InferredNode::Resolved { node: dt.clone() })), + span.clone(), + )), + LiteralBoundary::LiteralBoundaryRefused { message: m, .. } => { + Rc::new(InferResult { + typed: plain.clone(), + diagnostics: Rc::new(vec![inference_error( + m.clone(), + span.clone(), + scope.module_name.clone(), + )]), + }) + } + } } + ExprData::ExprElaboratedLiteral { .. } => ok_infer(texpr.clone()), ExprData::ExprError { kind, message, .. } => { let span = texpr.span.clone(); let diagnostics = match kind.clone() { @@ -9683,12 +10017,12 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), let span = texpr.span.clone(); let left_expr = crate::v1_std_core::binop_left(texpr.clone()); let right_expr = crate::v1_std_core::binop_right(texpr.clone()); - let left_result = - infer_expr(left_expr.clone(), scope.clone(), std::option::Option::None); + let operands = + infer_binop_operands(left_expr.clone(), right_expr.clone(), scope.clone()); + let left_result = operands.left.clone(); let left_typed = left_result.typed.clone(); let left_diags = left_result.diagnostics.clone(); - let right_result = - infer_expr(right_expr.clone(), scope.clone(), std::option::Option::None); + let right_result = operands.right.clone(); let right_typed = right_result.typed.clone(); let right_diags = right_result.diagnostics.clone(); let binop_info = crate::v1_compiler_infer_types::infer_binop_type_node( @@ -9701,6 +10035,11 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), Rc::new(ExprData::ExprBinOp { op: op.clone(), algebra_field: binop_info.algebra_field.clone(), + operand: operand_declaration_of_type( + crate::v1_compiler_infer_types::resolved_type(left_typed.clone()), + scope.clone(), + 8, + ), }), Rc::new(vec![left_typed.clone(), right_typed.clone()]), Some(Rc::new(InferredNode::Resolved { diff --git a/src/v1/stage0/src/v1_compiler_infer_env.rs b/src/v1/stage0/src/v1_compiler_infer_env.rs index 6d5ab844299..4103b09d53b 100644 --- a/src/v1/stage0/src/v1_compiler_infer_env.rs +++ b/src/v1/stage0/src/v1_compiler_infer_env.rs @@ -3,6 +3,8 @@ use self::GlobalBareLookupState::*; pub use crate::std_algebra::FreeMonoid; +pub use crate::std_decl_ref::decl_ref; +pub use crate::std_decl_ref::DeclarationRef; use crate::std_induction::RecursionShape::{ DirectRecursion, ListRecursion, MapValueRecursion, OptionalRecursion, SetRecursion, }; @@ -10,6 +12,7 @@ use crate::std_induction::SubValueRelation::{PreservedValue, SubValueUnknown}; pub use crate::std_induction::{InductiveField, RecursionShape, SubValueRelation}; pub use crate::std_occurrence_identity::NodeOccurrenceIdentity; use crate::std_occurrence_identity::NodeOccurrenceIdentity::OccurrenceSynthetic; +pub use crate::std_operator_realization::OperandDeclaration; pub use crate::std_types::is_kernel_type; pub use crate::std_types::SourceSpan; pub use crate::v1_compiler_infer_occurrence_binding::ModulePathBindingProjection; @@ -27,11 +30,11 @@ use crate::v1_std_core::Cardinality::*; use crate::v1_std_core::CompilerDiagnostic::{AmbiguousReference, UnresolvedType}; use crate::v1_std_core::Connective::*; use crate::v1_std_core::ExprData::*; -use crate::v1_std_core::InferredNode::*; +use crate::v1_std_core::InferredNode::Resolved; pub use crate::v1_std_core::{ authored_name_at, empty_intern_table, find_child_named, intern, intern_find, intern_str, kernel_span, merge_intern_tables, module_path_segments, param_node_name_at, - param_node_type_expr, source_text_at, + param_node_type_expr, qualified_last_segment, source_text_at, }; pub use crate::v1_std_core::{ Cardinality, CompilerDiagnostic, Connective, ExprData, InferredNode, InternTable, NewlineIndex, @@ -2142,3 +2145,96 @@ pub fn env_with_type_variable_bindings(env: Rc, tp_names: Rc, sp: Rc) -> bool { + match binding.resolved.clone().ident_span.clone() { + Some(s) => ((s.file.clone() == sp.file.clone()) && (s.start.clone() == sp.start.clone())), + None => false, + } +} + +pub fn type_reference_declaration( + n: Rc, + source_indices: Rc>>, + env: Rc, +) -> Option> { + { + let rt = match n.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { node: r, .. }) => r.clone(), + _ => match lookup_type_for(env.clone(), n.clone()) { + Some(bound) => bound.clone(), + None => n.clone(), + }, + }; + let decl_name = crate::v1_std_core::qualified_last_segment( + crate::v1_std_core::authored_name_at(source_indices.clone(), rt.clone()), + ); + if (decl_name.clone() == "".to_string()) { + return std::option::Option::None; + } + match rt.ident_span.clone() { + None => std::option::Option::None, + Some(sp) => match v1_rt::map_get( + &env.symbol_index.clone().global_bare.clone(), + decl_name.clone(), + ) + .as_deref() + .cloned() + { + Some(GlobalBareLookupState::GlobalBareUniqueBinding { + module_path: mp, + binding: b, + .. + }) => { + if binding_declares_span(b.clone(), sp.clone()) { + Some(Rc::new(OperandDeclaration { + declaration: crate::std_decl_ref::decl_ref( + mp.clone(), + decl_name.clone(), + ), + decl_file: sp.file.clone(), + })) + } else { + std::option::Option::None + } + } + Some(GlobalBareLookupState::GlobalBareAmbiguousBinding { + candidates: cands, + .. + }) => match Rc::new({ + let mut __result = Vec::new(); + for c in cands.iter().cloned() { + if binding_declares_span(c.binding.clone(), sp.clone()) { + __result.push(c); + } + } + __result + }) + .first() + .cloned() + { + Some(c) => Some(Rc::new(OperandDeclaration { + declaration: crate::std_decl_ref::decl_ref( + c.module_path.clone(), + decl_name.clone(), + ), + decl_file: sp.file.clone(), + })), + None => std::option::Option::None, + }, + None => std::option::Option::None, + }, + } + } +} + +pub fn type_reference_declaration_ref( + n: Rc, + source_indices: Rc>>, + env: Rc, +) -> Option> { + match type_reference_declaration(n.clone(), source_indices.clone(), env.clone()) { + Some(od) => Some(od.declaration.clone()), + None => std::option::Option::None, + } +} diff --git a/src/v1/stage0/src/v1_compiler_infer_resolve.rs b/src/v1/stage0/src/v1_compiler_infer_resolve.rs index bbb330650d8..80ae39d63c7 100644 --- a/src/v1/stage0/src/v1_compiler_infer_resolve.rs +++ b/src/v1/stage0/src/v1_compiler_infer_resolve.rs @@ -29,9 +29,10 @@ use crate::v1_std_core::CompilerDiagnostic::{ }; use crate::v1_std_core::Connective::{Arrow, Conj, Disj, NoConnective}; use crate::v1_std_core::ExprData::{ - ExprBinOp, ExprBlock, ExprCall, ExprCast, ExprError, ExprFieldAccess, ExprForEach, ExprIf, - ExprIndex, ExprLambda, ExprLet, ExprListLit, ExprLiteral, ExprMatch, ExprMethodCall, - ExprRecordLit, ExprReturn, ExprSlice, ExprStringInterp, ExprUnaryOp, ExprVar, NoExprData, + ExprBinOp, ExprBlock, ExprCall, ExprCast, ExprElaboratedLiteral, ExprError, ExprFieldAccess, + ExprForEach, ExprIf, ExprIndex, ExprLambda, ExprLet, ExprListLit, ExprLiteral, ExprMatch, + ExprMethodCall, ExprRecordLit, ExprReturn, ExprSlice, ExprStringInterp, ExprUnaryOp, ExprVar, + NoExprData, }; use crate::v1_std_core::ExprErrorKind::SemanticExprError; use crate::v1_std_core::InferredNode::{CompilerError, Resolved, TypeVariable}; @@ -2381,6 +2382,10 @@ pub fn resolve_expr_types( expr: texpr.clone(), diagnostics: Rc::new(vec![]), }), + ExprData::ExprElaboratedLiteral { .. } => Rc::new(ExprResolveResult { + expr: texpr.clone(), + diagnostics: Rc::new(vec![]), + }), ExprData::ExprError { kind, message, .. } => Rc::new(ExprResolveResult { expr: crate::v1_std_core::make_expr_error_node( Rc::new(NodeOccurrenceIdentity::OccurrenceSynthetic), @@ -2975,6 +2980,7 @@ pub fn resolve_expr_types( ExprData::ExprBinOp { op, algebra_field: af, + operand: od, .. } => { let ch = texpr.children.clone(); @@ -2998,6 +3004,7 @@ pub fn resolve_expr_types( Rc::new(ExprData::ExprBinOp { op: op.clone(), algebra_field: af.clone(), + operand: od.clone(), }), Rc::new(vec![lr.expr.clone(), rr.expr.clone()]), texpr.inferred.clone(), diff --git a/src/v1/stage0/src/v1_compiler_ownership.rs b/src/v1/stage0/src/v1_compiler_ownership.rs index 4a82b79ba34..d340561b89b 100644 --- a/src/v1/stage0/src/v1_compiler_ownership.rs +++ b/src/v1/stage0/src/v1_compiler_ownership.rs @@ -8,8 +8,9 @@ use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; use crate::v1_std_core::Cardinality::Required; use crate::v1_std_core::ExprData::{ - ExprBlock, ExprCall, ExprError, ExprFieldAccess, ExprForEach, ExprIf, ExprLambda, ExprLet, - ExprLiteral, ExprMatch, ExprMethodCall, ExprRecordLit, ExprReturn, ExprVar, NoExprData, + ExprBlock, ExprCall, ExprElaboratedLiteral, ExprError, ExprFieldAccess, ExprForEach, ExprIf, + ExprLambda, ExprLet, ExprLiteral, ExprMatch, ExprMethodCall, ExprRecordLit, ExprReturn, + ExprVar, NoExprData, }; use crate::v1_std_core::InferredNode::Resolved; use crate::v1_std_core::VarBindingKind::{FunctionValueBinding, LocalValueBinding}; @@ -309,6 +310,7 @@ pub fn walk_expr( } } ExprData::ExprLiteral { value: _, .. } => accum.clone(), + ExprData::ExprElaboratedLiteral { .. } => accum.clone(), ExprData::ExprFieldAccess { .. } => { let base_node = crate::v1_std_core::field_access_base(texpr.clone()); match (*base_node.expr_data.clone()).clone() { @@ -854,6 +856,7 @@ pub fn collect_callable_refs( _ => v1_rt::rc_empty_set::(), }, ExprData::ExprLiteral { value: _, .. } => v1_rt::rc_empty_set::(), + ExprData::ExprElaboratedLiteral { .. } => v1_rt::rc_empty_set::(), ExprData::ExprFieldAccess { .. } => collect_callable_refs( crate::v1_std_core::field_access_base(texpr.clone()), si.clone(), diff --git a/src/v1/stage0/src/v1_compiler_parse.rs b/src/v1/stage0/src/v1_compiler_parse.rs index 198c7cb3c54..217508d6b89 100644 --- a/src/v1/stage0/src/v1_compiler_parse.rs +++ b/src/v1/stage0/src/v1_compiler_parse.rs @@ -12391,6 +12391,8 @@ pub fn parse_expr_loop( op: binop.clone(), algebra_field: std::option::Option::None, + operand: + std::option::Option::None, }), Rc::new(vec![ lhs.clone(), @@ -14261,6 +14263,8 @@ pub fn parse_expr_loop_no_brace( op: binop.clone(), algebra_field: std::option::Option::None, + operand: + std::option::Option::None, }), Rc::new(vec![ lhs.clone(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 0dfcb912396..4269873649f 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -5019,6 +5019,15 @@ fn eval_expr_inner(node: &Rc, env: &Rc, ctx: &InterpContext) -> Inter match (*node.expr_data).clone() { ExprData::ExprLiteral { value } => eval_literal(&value), + // An elaborated literal (std.literal_elaboration) evaluates as the kernel value: this + // interpreter realizes the structural destinations natively by its own grounding + // (Zero/Succ as Int per #5428, v2.std.logic Bool as bool), so the image of the literal + // under that grounding IS the literal, and evaluating the constructor tree instead would + // route a natively-realized Bool through variant patterns that have no runtime form here. + // The structural image is consumed by emission, which is where the destination is + // structural; the emitted-bytes witnesses exercise that path. + ExprData::ExprElaboratedLiteral { value, .. } => eval_literal(&value), + ExprData::ExprVar { binding_kind } => eval_var(node, binding_kind.as_deref(), env, ctx), ExprData::ExprBinOp { op, .. } => { @@ -9938,6 +9947,7 @@ pub(crate) fn expr_data_form_name(expr_data: &ExprData) -> &'static str { match expr_data { ExprData::NoExprData => "NoExprData", ExprData::ExprLiteral { .. } => "ExprLiteral", + ExprData::ExprElaboratedLiteral { .. } => "ExprElaboratedLiteral", ExprData::ExprError { .. } => "ExprError", ExprData::ExprVar { .. } => "ExprVar", ExprData::ExprFieldAccess { .. } => "ExprFieldAccess", @@ -16451,7 +16461,7 @@ pub fn list_cons_tail_split_snapshot() -> (u64, u64) { ) } -pub const EXPR_VARIANT_COUNT: usize = 22; +pub const EXPR_VARIANT_COUNT: usize = 23; fn expr_variant_index(d: &ExprData) -> usize { match d { @@ -16477,6 +16487,7 @@ fn expr_variant_index(d: &ExprData) -> usize { ExprData::ExprIndex => 19, ExprData::ExprSlice => 20, ExprData::ExprReturn => 21, + ExprData::ExprElaboratedLiteral { .. } => 22, } } @@ -16504,6 +16515,7 @@ pub fn expr_variant_name(i: usize) -> &'static str { "ExprIndex", "ExprSlice", "ExprReturn", + "ExprElaboratedLiteral", ]; NAMES.get(i).copied().unwrap_or("?") } diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index 7c389bb4f86..3eecf328ede 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -29,6 +29,7 @@ use crate::std_algebra::CostShape::*; pub use crate::std_algebra::{AlgebraFieldTemplate, CollectionSizeEffect, CostShape}; pub use crate::std_induction::SubValueRelation; use crate::std_induction::SubValueRelation::*; +pub use crate::std_literal_elaboration::LiteralElaboration; use crate::std_occurrence_identity::NodeOccurrenceIdentity::OccurrenceSynthetic; use crate::std_occurrence_identity::OccurrenceTransportRefusal::{ DuplicateAuthoredOccurrenceIdentity, DuplicateSuppliedCandidateIdentity, @@ -43,6 +44,7 @@ pub use crate::std_occurrence_identity::{ AuthoredTokenOrdinalSpace, NodeOccurrenceIdentity, OccurrenceIdAllocator, OccurrenceTransportRefusal, }; +pub use crate::std_operator_realization::OperandDeclaration; pub use crate::std_source_annotation::AnnotationAttachmentRefusal; use crate::std_source_annotation::AnnotationAttachmentRefusal::*; pub use crate::std_source_annotation::{ @@ -300,6 +302,10 @@ pub enum ExprData { ExprLiteral { value: Rc, }, + ExprElaboratedLiteral { + value: Rc, + elaboration: Rc, + }, ExprError { kind: ExprErrorKind, message: String, @@ -327,6 +333,7 @@ pub enum ExprData { ExprBinOp { op: BinOp, algebra_field: Option, + operand: Option>, }, ExprUnaryOp { op: UnaryOpKind, @@ -2859,6 +2866,10 @@ pub fn expr_literal_int_optional(expr: Rc) -> Option { LiteralValue::LitInt { value: v, .. } => Some(v.clone()), _ => std::option::Option::None, }, + ExprData::ExprElaboratedLiteral { value: lit, .. } => match (*lit.clone()).clone() { + LiteralValue::LitInt { value: v, .. } => Some(v.clone()), + _ => std::option::Option::None, + }, ExprData::ExprUnaryOp { op: UnaryOpKind::Neg, .. @@ -2902,6 +2913,9 @@ pub fn expr_is_any_literal(mut expr: Rc) -> bool { break true; } }, + ExprData::ExprElaboratedLiteral { .. } => { + break true; + } ExprData::ExprUnaryOp { op: UnaryOpKind::Neg, .. @@ -3369,6 +3383,7 @@ pub fn expr_has_non_tail_self_call( binding_kind: _, .. } => false, ExprData::ExprLiteral { value: _, .. } => false, + ExprData::ExprElaboratedLiteral { .. } => false, ExprData::ExprFieldAccess { summary: _, .. } => { let mut __found = false; for child in texpr.children.clone().iter().cloned() { diff --git a/src/v2/std/integer.dag b/src/v2/std/integer.dag index 17aec4a2b12..e378900fc3f 100644 --- a/src/v2/std/integer.dag +++ b/src/v2/std/integer.dag @@ -29,7 +29,7 @@ import v2.std.machine { Word64, Word128 } -import v2.std.nat { Nat } +import v2.std.nat { Nat, Zero, Succ, NatQuotient, nat_div_rem_by_succ } import v2.std.text { Char, CharAbsent, CharFound, String, string_head, string_tail } type Int = GroupCompletion type UInt = v2.std.nat.Nat @@ -1306,41 +1306,97 @@ fn integer_signed_i32_le_bytes_to_int(bytes: List) -> Outcome { } } +// ONE GLYPH TABLE for the ten decimal digits, keyed on the DecimalDigit coproduct this module +// already owns; both the Peano and the machine-integer renderings below reach it through their +// own digit selection rather than each carrying a second copy of the ten glyphs. +fn decimal_digit_glyph(d: DecimalDigit) -> String { + match d { + D0 => "0" + D1 => "1" + D2 => "2" + D3 => "3" + D4 => "4" + D5 => "5" + D6 => "6" + D7 => "7" + D8 => "8" + D9 => "9" + } +} + +// The Peano value of each decimal digit. Every arm is a kernel integer literal at a +// v2.std.nat.Nat return boundary: the literal elaborates through the declared homomorphism +// (gunbc.structural_realization_bindings literal_homomorphism_rows) to its Zero/Succ image -- +// this function is the return-position exemplar of std.literal_elaboration. +fn decimal_digit_nat(d: DecimalDigit) -> v2.std.nat.Nat { + match d { + D0 => 0 + D1 => 1 + D2 => 2 + D3 => 3 + D4 => 4 + D5 => 5 + D6 => 6 + D7 => 7 + D8 => 8 + D9 => 9 + } +} + +// A Peano digit (a Nat below ten) to its glyph: select the DecimalDigit whose Peano value equals +// the digit by STRUCTURAL equality (std.operator_realization StructuralEquality on v2.std.nat.Nat), +// then read the one glyph table. A digit outside the roster (ten or more) is not a decimal digit +// and this function is not its authority: the caller obtains digits from nat_div_rem_by_succ by +// ten, whose remainder is below ten by construction, so the fold's D0 seed is never the answer +// for an in-domain input. fn integer_nat_decimal_digit_char(digit: v2.std.nat.Nat) -> String { - if digit == 0 { - "0" - } else if digit == 1 { - "1" - } else if digit == 2 { - "2" - } else if digit == 3 { - "3" - } else if digit == 4 { - "4" - } else if digit == 5 { - "5" - } else if digit == 6 { - "6" - } else if digit == 7 { - "7" - } else if digit == 8 { - "8" + decimal_digit_glyph(d: fold_list( + xs: decimal_digit_roster, + empty: D0, + cons: fn(acc, d) { if decimal_digit_nat(d: d) == digit { d } else { acc } } + )) +} + +// PEANO NAT TO DECIMAL TEXT over the DECLARED structural operations: division by ten is +// nat_div_rem_by_succ with divisor predecessor nine (the divisor Succ { prev: 9 } is nonzero by +// construction, so no zero-divisor arm exists to be handled), and the recursion descends on the +// quotient. The literal 9 elaborates at the argument boundary (std.literal_elaboration). No host +// operator is applied to a Nat here: the previous body spelled `value == 0`, `value < 10`, +// `value / 10` and `value - (rest * 10)` on Rc, which rustc refused (E0308 x10, E0369) and +// which the operator realization authority now refuses at emission by typed diagnostic instead. +fn integer_nat_to_decimal_string(value: v2.std.nat.Nat) -> String { + let q = nat_div_rem_by_succ(a: value, divisor_prev: 9) + match q.quotient { + Zero => integer_nat_decimal_digit_char(digit: q.remainder) + Succ { prev: _ } => + concat( + integer_nat_to_decimal_string(value: q.quotient), + integer_nat_decimal_digit_char(digit: q.remainder) + ) + } +} + +// MACHINE INTEGER TO DECIMAL TEXT. Int realizes as the host integer, so host division and +// remainder are its declared operations (std.operator_realization HostOperator); the digit glyph +// comes from the same one table. This is the formatter the two Int-valued callers that previously +// passed an Int into the Nat renderer's parameter (v2.std.native_agreement octet_display, +// v2.workflow.realization_sweep sweep_histogram_tsv) actually asked for -- the interpreter's +// numeric grounding made that mismatch invisible there, and the emitted closure refused it +// (E0308 Rc vs integer). +fn integer_int_to_decimal_string(value: Int) -> String { + if value < 0 { + concat("-", integer_int_magnitude_to_decimal_string(value: 0 - value)) } else { - "9" + integer_int_magnitude_to_decimal_string(value: value) } } -fn integer_nat_to_decimal_string(value: v2.std.nat.Nat) -> String { - if value == 0 { - "0" - } else if value < 10 { - integer_nat_decimal_digit_char(digit: value) +fn integer_int_magnitude_to_decimal_string(value: Int) -> String { + let rest = value / 10 + let digit = decimal_digit_glyph(d: decimal_digit_of_units(value: value - (rest * 10))) + if rest == 0 { + digit } else { - let rest = value / 10 - let digit = value - (rest * 10) - concat( - integer_nat_to_decimal_string(value: rest), - integer_nat_decimal_digit_char(digit: digit) - ) + concat(integer_int_magnitude_to_decimal_string(value: rest), digit) } } diff --git a/src/v2/std/nat.dag b/src/v2/std/nat.dag index 70218c5b9e4..7df36b11083 100644 --- a/src/v2/std/nat.dag +++ b/src/v2/std/nat.dag @@ -26,15 +26,78 @@ fn nat_mul(a: Nat, b: Nat) -> Nat { nat_cata(n: a, zero: Zero, succ: fn(acc) { nat_add(a: b, b: acc) }) } +// THE DECLARED ORDERING OF THE PEANO NATURALS, by exact operand structure: two Zeros are Equal, +// Zero precedes any Succ, and two Succs compare as their predecessors. This is the comparison the +// operator realization authority calls for `<`, `<=`, `>`, `>=` on v2.std.nat.Nat operands +// (gunbc.structural_realization_bindings structural_ordering_rows -> std.operator_realization), +// so it must not itself be written with a host ordering operator on Nat -- the previous body +// (`if a == b .. if a < b`) was exactly the host `<` on Rc that rustc refused (E0369). fn nat_compare(a: Nat, b: Nat) -> Ordering { - if a == b { - Equal - } else { - if a < b { - Less - } else { - Greater - } + match a { + Zero => + match b { + Zero => Equal + Succ { prev: _ } => Less + } + Succ { prev: pa } => + match b { + Zero => Greater + Succ { prev: pb } => nat_compare(a: pa, b: pb) + } + } +} + +// TRUNCATED SUBTRACTION (monus) WITH A TYPED UNDERFLOW OUTCOME. The naturals are not closed under +// subtraction; a - b for b > a has no answer here and says so as its own arm, never a wrapped or +// fabricated Zero. +type NatSubtraction + = NatDifference { value: Nat } + | NatSubtrahendExceedsMinuend + +fn nat_sub(a: Nat, b: Nat) -> NatSubtraction { + match b { + Zero => NatDifference { value: a } + Succ { prev: pb } => + match a { + Zero => NatSubtrahendExceedsMinuend + Succ { prev: pa } => nat_sub(a: pa, b: pb) + } + } +} + +// EUCLIDEAN DIVISION WITH A TYPED ZERO-DIVISOR OUTCOME. nat_div_rem is the general operation: a +// Zero divisor is its own arm. nat_div_rem_by_succ is the TOTAL form for a divisor that is nonzero +// BY CONSTRUCTION -- the caller supplies the divisor's predecessor, so the divisor Succ { prev } +// cannot be Zero and no zero-divisor arm exists to handle (DESIGN section 4b, the top rung: the +// invalid state has no constructor). A caller dividing by a literal that it knows is nonzero +// (decimal conversion by ten) uses the by-succ form rather than matching a zero arm it cannot reach. +type NatQuotient { + quotient: Nat + remainder: Nat +} + +type NatDivision + = NatQuotientRemainder { quotient: Nat, remainder: Nat } + | NatDivisionByZero + +fn nat_div_rem(a: Nat, b: Nat) -> NatDivision { + match b { + Zero => NatDivisionByZero + Succ { prev: divisor_prev } => + let q = nat_div_rem_by_succ(a: a, divisor_prev: divisor_prev) + NatQuotientRemainder { quotient: q.quotient, remainder: q.remainder } + } +} + +fn nat_div_rem_by_succ(a: Nat, divisor_prev: Nat) -> NatQuotient { + nat_div_rem_by_succ_accumulate(a: a, divisor_prev: divisor_prev, quotient: Zero) +} + +fn nat_div_rem_by_succ_accumulate(a: Nat, divisor_prev: Nat, quotient: Nat) -> NatQuotient { + match nat_sub(a: a, b: Succ { prev: divisor_prev }) { + NatSubtrahendExceedsMinuend => NatQuotient { quotient: quotient, remainder: a } + NatDifference { value: rest } => + nat_div_rem_by_succ_accumulate(a: rest, divisor_prev: divisor_prev, quotient: Succ { prev: quotient }) } } @@ -53,8 +116,18 @@ fn nat_lte(a: Nat, b: Nat) -> Bool { } } -data nat_max_two_nat_authorities_note: String = "This is NOT a duplicate of std.nat nat_max, and the distinction is worth stating because the name alone suggests otherwise. std.nat Nat is CommutativeSemiring - an algebra alias whose max is written with the host comparison operators - while v2.std.nat Nat is the Peano coproduct Zero | Succ, and the two are different types that no single function can serve. So this sits beside nat_add and nat_mul, which are forked for exactly the same reason and were not remarked on. What IS a real defect is that two Nat authorities exist at all; it predates this declaration and is the numeric-tower grounding thread's subject, not something a max function can close. Because v1-seed function names are not module-scoped, a bare nat_max reference in any closure containing both modules is ambiguous and must be qualified - v2.lens.cost.valuation does exactly that. Dissolve-on: one Nat authority, at which point one of the two nat_max declarations goes with it." - +// NOT A DUPLICATE OF std.nat nat_max, and worth saying because the name alone suggests otherwise. +// std.nat Nat is CommutativeSemiring -- an algebra alias whose max is written with the +// host comparison operators -- while v2.std.nat Nat is the Peano coproduct Zero | Succ. They are +// different types that no single function can serve, so this sits beside nat_add and nat_mul, which +// are forked for the same reason. Because v1-seed function names are not module-scoped, a bare +// nat_max reference in any closure containing both modules is ambiguous and must be qualified -- +// v2.lens.cost.valuation does exactly that. +// +// That two Nat authorities exist at all is the real defect, and it is tracked as a guarantee stall +// rather than narrated here: gunbc.guarantee_rung_drop two_nat_authorities_stall carries the rung, +// ceiling and next-rung trigger. This annotation records only why the fork is not closable from a +// max function. fn nat_max(a: Nat, b: Nat) -> Nat { match nat_compare(a: a, b: b) { Less => b diff --git a/src/v2/std/native_agreement.dag b/src/v2/std/native_agreement.dag index 23bcc6780f7..3ebac19304c 100644 --- a/src/v2/std/native_agreement.dag +++ b/src/v2/std/native_agreement.dag @@ -11,7 +11,7 @@ import v2.std.optional { Absent } import v2.std.logic { Bool } -import v2.std.integer { integer_nat_to_decimal_string } +import v2.std.integer { integer_int_to_decimal_string } import v2.std.runtime { RuntimePrimitive, RuntimePrimitiveValue, RuntimeValue } import v2.std.text { String } @@ -31,13 +31,7 @@ type NativeAgreementDivergence { // std cannot import compiler back). fn octet_display(octet: Int) -> String { - if octet == 0 { - "0" - } else if octet == 1 { - "1" - } else { - integer_nat_to_decimal_string(value: octet) - } + integer_int_to_decimal_string(value: octet) } fn runtime_value_discriminant_octet(value: RuntimeValue) -> Optional { diff --git a/src/v2/test/claim/self_host/peano_nat_structural_realization_test.dag b/src/v2/test/claim/self_host/peano_nat_structural_realization_test.dag new file mode 100644 index 00000000000..fd6cf1cf98c --- /dev/null +++ b/src/v2/test/claim/self_host/peano_nat_structural_realization_test.dag @@ -0,0 +1,316 @@ +module v2.test.claim.self_host.peano_nat_structural_realization_test + +import std.types { Bool, Int, String, List } +import std.algebra { Ordering, Less, Equal, Greater } +import std.decl_ref { decl_ref } +import std.literal_elaboration { + KernelIntLiteral, KernelStringLiteral, KernelBoolLiteral, + LiteralHomomorphismFound, LiteralHomomorphismAbsent, LiteralHomomorphismAmbiguous, + DirectLiteral, ViaHomomorphism, LiteralElaborationRefused, + PeanoUnfold, BooleanUnfold, + literal_homomorphism_for, elaborate_literal_at +} +import std.operator_realization { + HostNumericOperand, StructuralOperand, OperandIdentityUnavailable, HostRealizedOperand, KernelMintedType, + UnnamedSynthesizedType, + OperandShapeFacts, OperandIdentityUnavailableAt, + HostOperator, StructuralEquality, StructuralComparison, OperatorRealizationRefused, + NoStructuralOperationDeclared, OrderingIs, OrderingIsNot, + operator_realization_for +} +import std.syntax { BinOp, Lt, Le, Gt, Ge, Eq, Div, Mod, Sub, And, Add } +import gunbc.structural_realization_bindings { literal_homomorphism_rows, structural_ordering_rows } +import v2.std.nat { + Nat, Zero, Succ, + NatDifference, NatSubtrahendExceedsMinuend, + NatQuotientRemainder, NatDivisionByZero, + nat_compare, nat_sub, nat_div_rem, nat_div_rem_by_succ +} +import v2.std.integer { integer_nat_to_decimal_string, integer_int_to_decimal_string, decimal_digit_nat, D0, D7 } + +// FALSIFIERS FOR THE STRUCTURAL PEANO NAT REALIZATION (XL-0N, adhoc-aec65f93-b00), the +// interpreter-executed half. The emitted-bytes half -- that a kernel literal at a v2.std.nat.Nat +// boundary renders as its Zero/Succ image, that `<` on Nat renders as a call to nat_compare tested +// against std.algebra Ordering, that infix arithmetic on Nat refuses in the emitted bytes -- lives +// in test.claim.self_host_peano_literal_operator_realization_witness_test, because it must run the +// production emitter through compile_dag_rust_emit_check. +// +// Two subjects here. (1) The declared structural operations on v2.std.nat.Nat behave on NONTRIVIAL +// Succ values -- not merely on Zero and one -- which is what a reader of `nat_compare` as a two-arm +// match would otherwise take on faith. (2) The generic authorities decide by the ROW and by exact +// identity: the same literal into the native std.nat.Nat is Direct, into the Peano v2.std.nat.Nat +// is ViaHomomorphism, and with the row REMOVED it is Direct again -- which is exactly the state in +// which the emitted bytes carried a bare digit against Rc (the E0308 identities of XL-0's +// census). That last row is the executable form of "removing the elaboration row brings the +// E0308 identities back": the decision the emitter consumes flips, so the bytes flip. + +fn three() -> Nat { Succ { prev: Succ { prev: Succ { prev: Zero } } } } +fn five() -> Nat { Succ { prev: Succ { prev: three() } } } +fn seven() -> Nat { Succ { prev: Succ { prev: five() } } } + +test fn nat_compare_orders_nontrivial_succ_values() -> Bool { + nat_compare(a: three(), b: five()) == Less + && nat_compare(a: five(), b: three()) == Greater + && nat_compare(a: five(), b: five()) == Equal + && nat_compare(a: Zero, b: three()) == Less + && nat_compare(a: three(), b: Zero) == Greater +} + +test fn nat_sub_answers_underflow_as_its_own_arm() -> Bool { + let difference_holds = match nat_sub(a: seven(), b: five()) { + NatDifference { value: d } => nat_compare(a: d, b: Succ { prev: Succ { prev: Zero } }) == Equal + NatSubtrahendExceedsMinuend => false + } + let underflow_holds = match nat_sub(a: three(), b: five()) { + NatDifference { value: _ } => false + NatSubtrahendExceedsMinuend => true + } + difference_holds && underflow_holds +} + +test fn nat_div_rem_divides_nontrivial_values() -> Bool { + match nat_div_rem(a: seven(), b: Succ { prev: Succ { prev: Zero } }) { + NatQuotientRemainder { quotient: q, remainder: r } => + nat_compare(a: q, b: three()) == Equal && nat_compare(a: r, b: Succ { prev: Zero }) == Equal + NatDivisionByZero => false + } +} + +test fn nat_div_rem_by_zero_is_typed() -> Bool { + match nat_div_rem(a: seven(), b: Zero) { + NatQuotientRemainder { quotient: _, remainder: _ } => false + NatDivisionByZero => true + } +} + +test fn nat_div_rem_by_succ_has_no_zero_arm_and_divides() -> Bool { + let q = nat_div_rem_by_succ(a: seven(), divisor_prev: Succ { prev: Succ { prev: Zero } }) + nat_compare(a: q.quotient, b: Succ { prev: Succ { prev: Zero } }) == Equal + && nat_compare(a: q.remainder, b: Succ { prev: Zero }) == Equal +} + +test fn nat_to_decimal_converts_nontrivial_values() -> Bool { + integer_nat_to_decimal_string(value: Zero) == "0" + && integer_nat_to_decimal_string(value: seven()) == "7" + && integer_nat_to_decimal_string(value: Succ { prev: Succ { prev: Succ { prev: seven() } } }) == "10" + && integer_nat_to_decimal_string(value: 23) == "23" +} + +test fn decimal_digit_nat_supplies_the_peano_value() -> Bool { + nat_compare(a: decimal_digit_nat(d: D0), b: Zero) == Equal + && nat_compare(a: decimal_digit_nat(d: D7), b: seven()) == Equal +} + +test fn int_to_decimal_is_the_machine_integer_formatter() -> Bool { + integer_int_to_decimal_string(value: 0) == "0" + && integer_int_to_decimal_string(value: 42) == "42" + && integer_int_to_decimal_string(value: 0 - 7) == "-7" + && integer_int_to_decimal_string(value: 1000) == "1000" +} + +// --------------------------------------------------------------------------------------------- +// The generic authorities, decided by row and by exact identity. +// --------------------------------------------------------------------------------------------- + +test fn peano_row_is_found_by_exact_destination() -> Bool { + match literal_homomorphism_for(rows: literal_homomorphism_rows, source_kind: KernelIntLiteral, destination: decl_ref(module_path: "v2.std.nat", decl_name: "Nat")) { + LiteralHomomorphismFound { row: r } => + match r.producer { + PeanoUnfold { zero: z, succ: s, prev_field: p } => + (z.decl_name as String) == "Zero" && (s.decl_name as String) == "Succ" && (p as String) == "prev" + BooleanUnfold { true_variant: _, false_variant: _ } => false + } + LiteralHomomorphismAbsent => false + LiteralHomomorphismAmbiguous { row_count: _ } => false + } +} + +// Same spelling, different declaration: the native std.nat Nat has no row and is Direct. +test fn same_spelling_native_declaration_is_direct() -> Bool { + match elaborate_literal_at(rows: literal_homomorphism_rows, source_kind: KernelIntLiteral, destination: decl_ref(module_path: "std.nat", decl_name: "Nat"), destination_realizes_natively: true) { + DirectLiteral => true + ViaHomomorphism { homomorphism: _ } => false + LiteralElaborationRefused { cause: _ } => false + } +} + +test fn peano_destination_elaborates_via_the_homomorphism() -> Bool { + match elaborate_literal_at(rows: literal_homomorphism_rows, source_kind: KernelIntLiteral, destination: decl_ref(module_path: "v2.std.nat", decl_name: "Nat"), destination_realizes_natively: false) { + DirectLiteral => false + ViaHomomorphism { homomorphism: h } => (h.destination.decl_name as String) == "Nat" + LiteralElaborationRefused { cause: _ } => false + } +} + +// THE ROW-REMOVAL FALSIFIER. With no rows the same boundary is Direct -- the literal stays a bare +// kernel digit, which against an Rc parameter is precisely the E0308 shape the census held. +test fn removing_the_row_returns_the_literal_to_direct() -> Bool { + match elaborate_literal_at(rows: [], source_kind: KernelIntLiteral, destination: decl_ref(module_path: "v2.std.nat", decl_name: "Nat"), destination_realizes_natively: false) { + DirectLiteral => true + ViaHomomorphism { homomorphism: _ } => false + LiteralElaborationRefused { cause: _ } => false + } +} + +// THE BOOL ROW (kernel true/false -> v2.std.logic.Bool, the structural coproduct): found by exact +// destination, Direct with the row removed, and Direct at the prelude std.types.Bool, which realizes +// natively and has no row. No Bool VARIANT is matched by name in this interpreter-run module -- the +// interpreter realizes Bool natively and has no runtime form for `True` patterns -- so the image +// (Bool::True / Bool::False in the emitted bytes) is asserted only on the emitted path, in +// test.claim.self_host_peano_literal_operator_realization_witness_test. +test fn bool_row_is_found_by_exact_destination() -> Bool { + match literal_homomorphism_for(rows: literal_homomorphism_rows, source_kind: KernelBoolLiteral, destination: decl_ref(module_path: "v2.std.logic", decl_name: "Bool")) { + LiteralHomomorphismFound { row: r } => + match r.producer { + BooleanUnfold { true_variant: t, false_variant: f } => (t.decl_name as String) == "True" && (f.decl_name as String) == "False" + PeanoUnfold { zero: _, succ: _, prev_field: _ } => false + } + LiteralHomomorphismAbsent => false + LiteralHomomorphismAmbiguous { row_count: _ } => false + } +} + +test fn removing_the_bool_row_returns_the_literal_to_direct() -> Bool { + match elaborate_literal_at(rows: [], source_kind: KernelBoolLiteral, destination: decl_ref(module_path: "v2.std.logic", decl_name: "Bool"), destination_realizes_natively: false) { + DirectLiteral => true + ViaHomomorphism { homomorphism: _ } => false + LiteralElaborationRefused { cause: _ } => false + } +} + +test fn prelude_bool_destination_is_direct() -> Bool { + match elaborate_literal_at(rows: literal_homomorphism_rows, source_kind: KernelBoolLiteral, destination: decl_ref(module_path: "std.types", decl_name: "Bool"), destination_realizes_natively: true) { + DirectLiteral => true + ViaHomomorphism { homomorphism: _ } => false + LiteralElaborationRefused { cause: _ } => false + } +} + +// A kernel STRING literal into the Peano Nat has no row: the source kind is part of the key. +test fn source_kind_is_part_of_the_key() -> Bool { + match literal_homomorphism_for(rows: literal_homomorphism_rows, source_kind: KernelStringLiteral, destination: decl_ref(module_path: "v2.std.nat", decl_name: "Nat")) { + LiteralHomomorphismFound { row: _ } => false + LiteralHomomorphismAbsent => true + LiteralHomomorphismAmbiguous { row_count: _ } => false + } +} + +// Two rows for one key refuse rather than picking one. +test fn duplicated_row_refuses() -> Bool { + let doubled = concat(literal_homomorphism_rows, literal_homomorphism_rows) + match elaborate_literal_at(rows: doubled, source_kind: KernelIntLiteral, destination: decl_ref(module_path: "v2.std.nat", decl_name: "Nat"), destination_realizes_natively: false) { + DirectLiteral => false + ViaHomomorphism { homomorphism: _ } => false + LiteralElaborationRefused { cause: _ } => true + } +} + +test fn ordering_on_the_peano_operand_calls_the_declared_comparison() -> Bool { + let nat = decl_ref(module_path: "v2.std.nat", decl_name: "Nat") + match operator_realization_for(op: Lt, operand: StructuralOperand { declaration: nat }, ordering_rows: structural_ordering_rows) { + StructuralComparison { declaration: _, binding: b, test: t } => + (b.compare.decl_name as String) == "nat_compare" + && (b.ordering.module_path as String) == "std.algebra" + && match t { OrderingIs { variant: v } => (v as String) == "Less" OrderingIsNot { variant: _ } => false } + _ => false + } +} + +test fn non_strict_ordering_negates_the_opposite_variant() -> Bool { + let nat = decl_ref(module_path: "v2.std.nat", decl_name: "Nat") + match operator_realization_for(op: Le, operand: StructuralOperand { declaration: nat }, ordering_rows: structural_ordering_rows) { + StructuralComparison { declaration: _, binding: _, test: t } => + match t { OrderingIs { variant: _ } => false OrderingIsNot { variant: v } => (v as String) == "Greater" } + _ => false + } +} + +test fn equality_on_the_peano_operand_is_structural() -> Bool { + match operator_realization_for(op: Eq, operand: StructuralOperand { declaration: decl_ref(module_path: "v2.std.nat", decl_name: "Nat") }, ordering_rows: structural_ordering_rows) { + StructuralEquality { declaration: d } => (d.decl_name as String) == "Nat" + _ => false + } +} + +// FORCING HOST ARITHMETIC ONTO A PEANO OPERAND REDS: the decision refuses, typed, naming the +// declaration and the operator. The emitted-bytes form of this row is in the emit-check witness. +fn host_arithmetic_on_peano_refuses(op: BinOp) -> Bool { + match operator_realization_for(op: op, operand: StructuralOperand { declaration: decl_ref(module_path: "v2.std.nat", decl_name: "Nat") }, ordering_rows: structural_ordering_rows) { + OperatorRealizationRefused { cause: NoStructuralOperationDeclared { declaration: d, operator: _ } } => (d.decl_name as String) == "Nat" + _ => false + } +} + +test fn host_arithmetic_on_the_peano_operand_refuses() -> Bool { + host_arithmetic_on_peano_refuses(op: Div) && host_arithmetic_on_peano_refuses(op: Mod) && host_arithmetic_on_peano_refuses(op: Sub) +} + +// A structural declaration with NO ordering row refuses `<` rather than emitting the host token. +test fn ordering_without_a_declared_comparison_refuses() -> Bool { + match operator_realization_for(op: Gt, operand: StructuralOperand { declaration: decl_ref(module_path: "v2.std.text", decl_name: "String") }, ordering_rows: structural_ordering_rows) { + OperatorRealizationRefused { cause: _ } => true + _ => false + } +} + +test fn host_numeric_operand_keeps_the_host_operator() -> Bool { + let native_holds = match operator_realization_for(op: Div, operand: HostNumericOperand, ordering_rows: structural_ordering_rows) { + HostOperator => true + _ => false + } + let by_construction_holds = match operator_realization_for(op: Ge, operand: HostRealizedOperand { reason: KernelMintedType }, ordering_rows: structural_ordering_rows) { + HostOperator => true + _ => false + } + native_holds && by_construction_holds +} + +// AN OPERAND WHOSE DECLARATION COULD NOT BE READ REFUSES, carrying what the caller saw. The seed's +// host-token fallback here was an absorbing arm (DESIGN section 5): it rendered `a < b` on a Peano +// operand as the host `<` with no signature, and the lane's own emitted-path rows went red on a +// token rustc refuses later. This row pins that the unknown arm is a refusal, not a widen. +test fn operand_without_a_readable_declaration_refuses() -> Bool { + let facts = OperandShapeFacts { authored_name: "Nat", connective: "NoConnective", child_count: 0, resolved: false, decl_file: "probe.dag" } + let ordering_refuses = match operator_realization_for(op: Lt, operand: OperandIdentityUnavailable { facts: facts }, ordering_rows: structural_ordering_rows) { + OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: o, facts: f } } => + match o { Lt => f.authored_name == "Nat" _ => false } + _ => false + } + let arithmetic_refuses = match operator_realization_for(op: Div, operand: OperandIdentityUnavailable { facts: facts }, ordering_rows: structural_ordering_rows) { + OperatorRealizationRefused { cause: OperandIdentityUnavailableAt { operator: o, facts: _ } } => + match o { Div => true _ => false } + _ => false + } + ordering_refuses && arithmetic_refuses +} + +// AN UNNAMED SYNTHESIZED TYPE NODE IS HOST BY CONSTRUCTION UNDER EVERY OPERATOR, including the +// arithmetic ones that refuse on a NAMED unreadable declaration. A structural declaration is reached +// by a name, so a node with none is not a reference to one -- the discriminator, not a catch-all. +// Its live subject is v2.compiler.02_parse parse_current_position (`t.start + 1`, t bound by a +// match arm over the generic ListHeadResult), which this lane's own refusal arm reddened before +// the arm was narrowed to named operands. +test fn an_unnamed_synthesized_operand_is_host_under_arithmetic() -> Bool { + match operator_realization_for(op: Add, operand: HostRealizedOperand { reason: UnnamedSynthesizedType }, ordering_rows: structural_ordering_rows) { + HostOperator => true + _ => false + } +} + +// EQUALITY ON THE SAME OPERAND IS THE HOST TOKEN BY CONSTRUCTION: structural and host equality are +// one token on the target, so the decision does not need the declaration. This is a decided arm, +// not the widen above -- ordering on the same operand refuses (the row before this one). +test fn equality_without_a_readable_declaration_is_host_by_construction() -> Bool { + let facts = OperandShapeFacts { authored_name: "", connective: "NoConnective", child_count: 0, resolved: true, decl_file: "" } + match operator_realization_for(op: Eq, operand: OperandIdentityUnavailable { facts: facts }, ordering_rows: structural_ordering_rows) { + HostOperator => true + _ => false + } +} + +test fn logical_connective_on_a_structural_operand_stays_host() -> Bool { + match operator_realization_for(op: And, operand: StructuralOperand { declaration: decl_ref(module_path: "v2.std.logic", decl_name: "Bool") }, ordering_rows: structural_ordering_rows) { + HostOperator => true + _ => false + } +} diff --git a/src/v2/workflow/floor_cost_debt.dag b/src/v2/workflow/floor_cost_debt.dag index 85945eb6d70..691dfea7062 100644 --- a/src/v2/workflow/floor_cost_debt.dag +++ b/src/v2/workflow/floor_cost_debt.dag @@ -135,7 +135,7 @@ import v2.std.text { String } // test.claim.callable_candidate_ambiguity_witness.a_listed_import_does_not_exclude_a_transitively_reached_homonym // test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_and_neither_mis_resolves // test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_natively_realized_nat_is_admitted -// test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_peano_nat_is_refused +// test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_peano_nat_is_admitted_through_its_homomorphism // test.claim.declared_type_inhabitance_list_element_witness.w_declared_coproduct_member_is_accepted // test.claim.declared_type_inhabitance_list_element_witness.w_optional_carrier_is_undecidable_not_refused // test.claim.declared_type_inhabitance_list_element_witness.w_reachability_control_discriminates_on_the_name diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index bbd05fae216..1c1cd022b05 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -528,8 +528,16 @@ fn floor_expected_red_chunk_13() -> List { // THE PROSE ABOVE PREDICTED BOTH ROWS WOULD GO GREEN TOGETHER. Wrong, and left on the record: it // read the two halves of its own trigger as one event. The mechanical repair and the // literal-introduction model are independent, and only the first is a predicate repair. +// RETIRED BY ITS TRIGGER (XL-0N, adhoc-aec65f93-b00): the expected-type-directed literal +// introduction judgment is std.literal_elaboration, consumed by v1.compiler.infer at every typed +// boundary, and the ruling (2026-08-30) admits the kernel numeral at the Peano Nat THROUGH its +// declared homomorphism rather than refusing it. The row's witness is renamed to the ruled claim +// (w_kernel_numeric_at_the_peano_nat_is_admitted_through_its_homomorphism) and stays enrolled as +// a permanent control beside the emitted-bytes falsifier in +// test.claim.self_host_peano_literal_operator_realization_witness_test. The chunk stays so the +// roster's shape is unchanged; it carries nothing. fn floor_expected_red_chunk_14() -> List { - Cons { head: "test.claim.declared_type_inhabitance_direct_call_witness.w_kernel_numeric_at_the_peano_nat_is_refused", tail: Empty {} } + Empty {} } // THE LIST-ELEMENT ARM OF THE DIRECT-CALL INHABITANCE WITNESS. It asserts that a wrong element diff --git a/src/v2/workflow/realization_sweep.dag b/src/v2/workflow/realization_sweep.dag index 4b499b48e3e..83972d7f7d4 100644 --- a/src/v2/workflow/realization_sweep.dag +++ b/src/v2/workflow/realization_sweep.dag @@ -27,7 +27,7 @@ import v2.compiler.source_authority_read { source_root_ingest_build_from_source_refs } import v2.std.compilers.lexing { symbol_intern_lexeme, symbol_lexeme } -import v2.std.integer { integer_nat_to_decimal_string } +import v2.std.integer { integer_int_to_decimal_string } import v2.std.optional { Optional, Present, Absent } import v2.std.algebra { fold_list, length } import v2.std.collection { list_at_optional } @@ -373,15 +373,15 @@ fn sweep_histogram_tsv(rows: List) -> String { SweepHistogramState { prev: k, count: 1, - out: if st.out == "" { concat(st.prev, "\t", integer_nat_to_decimal_string(value: st.count)) } else { concat(st.out, "\n", st.prev, "\t", integer_nat_to_decimal_string(value: st.count)) } + out: if st.out == "" { concat(st.prev, "\t", integer_int_to_decimal_string(value: st.count)) } else { concat(st.out, "\n", st.prev, "\t", integer_int_to_decimal_string(value: st.count)) } } } }) if folded.count == 0 { folded.out } else if folded.out == "" { - concat(folded.prev, "\t", integer_nat_to_decimal_string(value: folded.count)) + concat(folded.prev, "\t", integer_int_to_decimal_string(value: folded.count)) } else { - concat(folded.out, "\n", folded.prev, "\t", integer_nat_to_decimal_string(value: folded.count)) + concat(folded.out, "\n", folded.prev, "\t", integer_int_to_decimal_string(value: folded.count)) } } diff --git a/src/v2/workflow/rust_crate_partition.dag b/src/v2/workflow/rust_crate_partition.dag index 5bcc36d946f..e71e0612a93 100644 --- a/src/v2/workflow/rust_crate_partition.dag +++ b/src/v2/workflow/rust_crate_partition.dag @@ -252,6 +252,8 @@ fn stage0_std_core_modules() -> List { "std_occurrence_identity", "std_source_annotation", "std_target_representation", + "std_literal_elaboration", + "std_operator_realization", "v1_std_core" ]) } @@ -300,7 +302,7 @@ fn stage0_extdeps_modules() -> List { // the v1_compiler_* pipeline modules because the layer is a different one -- the // grouping is physical (one crate) while the name records what the module actually is. fn stage0_gunbc_binding_modules() -> List { - ["gunbc_rust_source_type_bindings"] + ["gunbc_rust_source_type_bindings", "gunbc_structural_realization_bindings"] } fn stage0_v1_infer_modules() -> List { @@ -448,6 +450,13 @@ fn stage0_cross_unit_import_edges() -> List { stage0_module_dag_edge(from: "extdeps_languages_rust_emit", to: "std_trait_derive_shape"), stage0_module_dag_edge(from: "std_source_annotation", to: "std_types"), stage0_module_dag_edge(from: "std_source_annotation", to: "std_occurrence_identity"), + stage0_module_dag_edge(from: "std_literal_elaboration", to: "std_decl_ref"), + stage0_module_dag_edge(from: "std_literal_elaboration", to: "std_syntax"), + stage0_module_dag_edge(from: "std_literal_elaboration", to: "std_types"), + stage0_module_dag_edge(from: "std_operator_realization", to: "std_decl_ref"), + stage0_module_dag_edge(from: "std_operator_realization", to: "std_syntax"), + stage0_module_dag_edge(from: "std_operator_realization", to: "std_types"), + stage0_module_dag_edge(from: "v1_std_core", to: "std_literal_elaboration"), stage0_module_dag_edge(from: "v1_std_core", to: "std_source_annotation"), stage0_module_dag_edge(from: "v1_std_core", to: "std_algebra"), stage0_module_dag_edge(from: "v1_std_core", to: "std_induction"),