diff --git a/dsl/shared/dag_util.dag b/dsl/shared/dag_util.dag index a3214713a9d..c33055db15e 100644 --- a/dsl/shared/dag_util.dag +++ b/dsl/shared/dag_util.dag @@ -15,10 +15,10 @@ import std.types { Document, DocumentLine, DocumentSection, + DocumentFile, RenderedTextFile, StageResult, Summary, - TextFile, TextFilePath } // --- Result aggregation ----------------------------------------------- @@ -73,7 +73,7 @@ fn generated_header(tool: String) -> String { } // --- Structured document rendering ------------------------------------- -// Shared "rendering engine" for Document/TextFile trees. +// Shared "rendering engine" for Document/DocumentFile trees. fn text_line(text: String) -> DocumentLine { { text: text, is_comment: false, is_blank: false } diff --git a/dsl/std/types.dag b/dsl/std/types.dag index e81b50254bf..d32f1be450d 100644 --- a/dsl/std/types.dag +++ b/dsl/std/types.dag @@ -547,7 +547,7 @@ type Document { trailing_newline: Bool } -type TextFile { +type DocumentFile { path: String document: Document } diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 514b4e83965..19d91715131 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2841,6 +2841,59 @@ fn record_lit_alias_struct_fields(type_name: String, scope: InferScope) -> List< } } +// Strict record construction (§5 fail-closed): the SOURCE field-name set of the concrete +// record a construction targets, or `none` whenever we cannot enumerate it with confidence — +// so the undefined-field check stays silent rather than false-positive. We fire ONLY when the +// constructed name resolves to a plain, fully-grounded record: non-generic (`params == 0`) and +// a direct product (`connective == Conj`) with declared fields. Everything else returns `none`: +// - generics (`Monoid`, `Vendor`): newtype flattening rewrites a single-field +// wrapper to its innermost name (`Monoid` resolves to `[op, identity]`, not `[semigroup, +// identity]`), so the resolved set is not source-faithful; +// - concrete aliases of single-field generics (`Watt = Measure`): the wrapper +// dissolves to its `` carrier, so the resolved node is not a record at all; +// - a name resolving to a coproduct/enum — including the losing side of a §3 name collision +// (the `Vendor` enum shadowing the `Vendor` record): no product fields to check. +// This keeps full teeth on plain records, where every real bug it finds lives (`BoolWitness +// { holds }`, `NodeLocus { node }`, `PortLocus { port }`). Dissolution trigger: when field-name +// resolution is source-faithful under flattening, widen the gate to generics and aliases. +fn record_lit_construction_field_names(type_name: String, scope: InferScope) -> List? { + let si = scope.type_env.source_indices + match lookup_type_by_name(env: scope.type_env, name: type_name) { + Present { value: decl } => + if (decl.params |> count == 0) && (decl.connective == Conj) && (decl.children |> count > 0) { + Present { value: decl.children |> map(f => authored_name_at(source_indices: si, node: f)) } + } else { + none + } + Absent => none + } +} + +// Strict record construction: a constructed NAME can legitimately arm two distinct coproducts +// with different field sets (e.g. `TextNode` is `Fragment.TextNode { content }` in one and +// `MarkupNode.TextNode { text }` in another). The import-scoped `struct_fields`/`arm_fields` +// only see the arm reachable from `expected`; this secondary scan, run ONLY on a would-be +// error, asks whether `field` is valid on a same-named arm of ANY coproduct in the env — so +// `TextNode { text }` stays silent when *some* `TextNode` arm has `text`, while a field present +// on NO same-named arm keeps its loud error (§5). Record-name collisions are NOT handled here: +// duplicate record names across layers are a §3 violation that must be de-conflicted at the +// source (cf. the `TextFile` → `DocumentFile` split), not papered over by a suppressor. +fn field_in_any_variant_named(type_name: String, field: String, scope: InferScope) -> Bool { + let si = scope.type_env.source_indices + scope.type_env.bindings |> map_values |> any(binding => + let node = binding.resolved + if (node.connective == Disj) { + node.children |> any(arm => + if authored_name_at(source_indices: si, node: arm) == type_name { + let ea = expand_type_for_field_access(n: arm, env: scope.type_env, module_name: scope.module_name) + let fields = if (ea.connective == Conj) { ea.children } else { arm.children } + fields |> any(f => authored_name_at(source_indices: si, node: f) == field) + } else { false } + ) + } else { false } + ) +} + fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpan, name_span: SourceSpan, scope: InferScope, expected: Node?) -> InferResult { let struct_fields = match type_name { Present { value: tn } => @@ -2870,8 +2923,29 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa } } } + let construction_field_names = match type_name { + Present { value: tn } => record_lit_construction_field_names(type_name: tn, scope: scope) + Absent => none + } + let tn_str = match type_name { + Present { value: tn } => tn + Absent => "" + } let fi_infer_results = map(field_inits, fi => let fi_name = field_init_node_name_at(n: fi, source_indices: scope.type_env.source_indices) + // Strict record construction (§5 fail-closed): a field that matches no field of a + // confidently-RESOLVED type is a loud, located error, not silently ignored. `none` + // (unresolved / generic / anonymous record) keeps the path silent — closes the + // fail-open `infer_record_lit` hole without false-positives. + let unknown_field_diags = match construction_field_names { + Present { value: names } => + if (names |> any(n => n == fi_name)) || field_in_any_variant_named(type_name: tn_str, field: fi_name, scope: scope) { + [] + } else { + [make_error_node(diagnostic: FieldNotFound { field: fi_name, type_name: tn_str, span: fi.span }, module_name: scope.module_name)] + } + Absent => [] + } let field_expected = match struct_fields |> filter(sf => authored_name_at(source_indices: scope.type_env.source_indices, node: sf) == fi_name) |> first { Present { value: sf } => let ft = match sf.inferred { @@ -2908,7 +2982,7 @@ fn infer_record_lit(type_name: String?, field_inits: List, span: SourceSpa FieldInferResult { typed_field: make_field_init_node(name: fi_name, value: ar_typed, span: fi.span, name_span: node_name_span(n: fi)), infer_result: ar, - diagnostics: concat(ar_diags, field_type_diags) + diagnostics: concat(concat(ar_diags, field_type_diags), unknown_field_diags) } ) let typed_fields = fi_infer_results |> map(fir => fir.typed_field) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 88f94cf7a6a..ec4d51a09a6 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -5465,6 +5465,100 @@ pub fn record_lit_alias_struct_fields( } } +pub fn record_lit_construction_field_names( + type_name: String, + scope: Rc, +) -> Option>> { + { + let si = scope.type_env.clone().source_indices.clone(); + match lookup_type_by_name(scope.type_env.clone(), type_name) { + Some(decl) => { + if ((((decl.params.clone().len() as i64) == 0) + && (decl.connective.clone() == Connective::Conj)) + && ((decl.children.clone().len() as i64) > 0)) + { + Some(Rc::new({ + let mut __result = Vec::new(); + for f in decl.children.clone().iter().cloned() { + __result.push(authored_name_at(si.clone(), f.clone())); + } + __result + })) + } else { + None + } + } + None => None, + } + } +} + +pub fn field_in_any_variant_named(type_name: String, field: String, scope: Rc) -> bool { + { + let si = scope.type_env.clone().source_indices.clone(); + { + let mut __found = false; + for binding in Rc::new(v1_rt::map_values(&scope.type_env.clone().bindings.clone())) + .iter() + .cloned() + { + if { + let node = binding.resolved.clone(); + if (node.connective.clone() == Connective::Disj) { + { + let mut __found = false; + for arm in node.children.clone().iter().cloned() { + if if (authored_name_at(si.clone(), arm.clone()).as_str() + == type_name.clone().as_str()) + { + { + let ea = expand_type_for_field_access( + arm.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + let fields = if (ea.connective.clone() == Connective::Conj) + { + ea.children.clone() + } else { + arm.children.clone() + }; + { + let mut __found = false; + for f in fields.clone().iter().cloned() { + if (authored_name_at(si.clone(), f.clone()) + .as_str() + == field.clone().as_str()) + { + __found = true; + break; + } + } + __found + } + } + } else { + false + } { + __found = true; + break; + } + } + __found + } + } else { + false + } + } { + __found = true; + break; + } + } + __found + } + } +} + pub fn infer_record_lit( type_name: Option, field_inits: Rc>>, @@ -5512,6 +5606,14 @@ pub fn infer_record_lit( }, }, }; + let construction_field_names = match type_name.clone() { + Some(tn) => record_lit_construction_field_names(tn.clone(), scope.clone()), + None => None, + }; + let tn_str = match type_name.clone() { + Some(tn) => tn.clone(), + None => "".to_string(), + }; let fi_infer_results = Rc::new({ let mut __result = Vec::new(); for fi in field_inits.iter().cloned() { @@ -5520,6 +5622,36 @@ pub fn infer_record_lit( fi.clone(), scope.type_env.clone().source_indices.clone(), ); + let unknown_field_diags = match construction_field_names.clone() { + Some(names) => { + if ({ + let mut __found = false; + for n in names.clone().iter().cloned() { + if (n.clone().as_str() == fi_name.clone().as_str()) { + __found = true; + break; + } + } + __found + } || field_in_any_variant_named( + tn_str.clone(), + fi_name.clone(), + scope.clone(), + )) { + Rc::new(vec![]) + } else { + Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::FieldNotFound { + field: fi_name.clone(), + type_name: tn_str.clone(), + span: fi.span.clone(), + }), + scope.module_name.clone(), + )]) + } + } + None => Rc::new(vec![]), + }; let field_expected = match Rc::new({ let mut __result = Vec::new(); for sf in struct_fields.clone().iter().cloned() { @@ -5594,7 +5726,10 @@ pub fn infer_record_lit( node_name_span(fi.clone()), ), infer_result: ar.clone(), - diagnostics: v1_rt::concat(ar_diags.clone(), field_type_diags.clone()), + diagnostics: v1_rt::concat( + v1_rt::concat(ar_diags.clone(), field_type_diags.clone()), + unknown_field_diags.clone(), + ), }) }); } diff --git a/src/v2/compiler/manual/infer_ground_add_mvp.dag b/src/v2/compiler/manual/infer_ground_add_mvp.dag index 4507493f0fa..581ac856f38 100644 --- a/src/v2/compiler/manual/infer_ground_add_mvp.dag +++ b/src/v2/compiler/manual/infer_ground_add_mvp.dag @@ -124,7 +124,7 @@ fn infer_receipt_runtime_value() -> RuntimeValue { fn infer_receipt_runtime_diagnostic(n: Node) -> Diagnostic { Diagnostic { reason: ^infer_receipt_extdeps, - at: NodeLocus { node: n }, + at: node_locus(node: n), correction: Unavailable { reason: AmbiguousIntent } } } diff --git a/src/v2/extdeps/formats/spice_passive_projection_test.dag b/src/v2/extdeps/formats/spice_passive_projection_test.dag index 597b442451e..9dcc73d7891 100644 --- a/src/v2/extdeps/formats/spice_passive_projection_test.dag +++ b/src/v2/extdeps/formats/spice_passive_projection_test.dag @@ -22,16 +22,6 @@ import v2.std.timeseries_signal { InductorPassive, ResistorPassive, } -import v2.std.verification { - BoolWitness, - BoolWitnessClaim, - ManualAnchorAbsent, - TestClaim, - TestClassification, - Tier1, - Unit, - manual_claim_anchor -} test fn spice_resistor_projects_resistor_passive_topology_holds() -> Bool { let component = Resistor { @@ -84,31 +74,3 @@ test fn passive_topology_preserves_component_name_holds() -> Bool { Absent => false } } - -data claim_spice_resistor_passive_spec: TestClaim = BoolWitnessClaim { - label: "extdeps/formats/spice_passive_projection: spice Resistor projects ResistorPassive topology", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: spice_resistor_projects_resistor_passive_topology_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_spice_capacitor_passive_arm: TestClaim = BoolWitnessClaim { - label: "extdeps/formats/spice_passive_projection: spice Capacitor projects CapacitorPassive arm", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: spice_capacitor_projects_capacitor_passive_arm_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_spice_inductor_passive_arm: TestClaim = BoolWitnessClaim { - label: "extdeps/formats/spice_passive_projection: spice Inductor projects InductorPassive arm", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: spice_inductor_projects_inductor_passive_arm_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} - -data claim_passive_topology_preserves_name: TestClaim = BoolWitnessClaim { - label: "extdeps/formats/spice_passive_projection: passive_topology_from_component preserves name", - anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), - witness: BoolWitness { holds: passive_topology_preserves_component_name_holds() }, - classification: TestClassification { tier: Tier1, layer: Unit } -} diff --git a/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag b/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag index d423d677a80..9f0e0cbd004 100644 --- a/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag +++ b/src/v2/lens/application/apply_lens_introspect_rejection_is_advisory.dag @@ -10,7 +10,7 @@ import v2.compiler.compile { compile_lens_gate_rejected_diagnostic } import v2.compiler.infer { InferredTree } -import v2.std.diagnostic { Accepted, Diagnostics, None, Outcome, PortLocus, Rejected, Some, outcome_rejected } +import v2.std.diagnostic { Accepted, Diagnostics, None, Outcome, Rejected, Some, outcome_rejected, port_locus } import v2.std.logic { Bool } import v2.std.node { Atom, Conj, Node, Symbol, TypeNode, SyntheticOccurrence } import v2.std.verification { @@ -43,7 +43,7 @@ fn apply_lens_mode_tree() -> InferredTree { fn apply_lens_mode_rejecting_gate(_tree: InferredTree) -> Outcome> { outcome_rejected( - compile_lens_gate_rejected_diagnostic(at: PortLocus { port: ^apply_lens_mode_gate_at }) + compile_lens_gate_rejected_diagnostic(at: port_locus(port: ^apply_lens_mode_gate_at)) ) } diff --git a/src/v2/lens/application/enforce_rejecting_gate_fires.dag b/src/v2/lens/application/enforce_rejecting_gate_fires.dag index 759beffb57b..4f5e993d458 100644 --- a/src/v2/lens/application/enforce_rejecting_gate_fires.dag +++ b/src/v2/lens/application/enforce_rejecting_gate_fires.dag @@ -8,7 +8,7 @@ import v2.compiler.compile { compile_lens_gate_rejected_diagnostic } import v2.compiler.infer { InferredTree } -import v2.std.diagnostic { Accepted, Outcome, PortLocus, Rejected, outcome_rejected } +import v2.std.diagnostic { Accepted, Outcome, Rejected, outcome_rejected, port_locus } import v2.std.logic { Bool } import v2.std.node { Atom, Conj, Node, Symbol, TypeNode, SyntheticOccurrence } import v2.std.verification { @@ -41,7 +41,7 @@ fn enforce_reject_tree() -> InferredTree { fn enforce_rejecting_gate(_tree: InferredTree) -> Outcome> { outcome_rejected( - compile_lens_gate_rejected_diagnostic(at: PortLocus { port: ^enforce_reject_gate_at }) + compile_lens_gate_rejected_diagnostic(at: port_locus(port: ^enforce_reject_gate_at)) ) } diff --git a/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag b/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag index 06fe3d7c6f2..91580a6d730 100644 --- a/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag +++ b/src/v2/lens/application/rejecting_lens_blocks_before_compile.dag @@ -14,7 +14,7 @@ import v2.compiler.infer { InferredTree } import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms_empty } import v2.std.compilers.lexing { VoidLexRules } import v2.std.collection { empty_map } -import v2.std.diagnostic { Accepted, Outcome, PortLocus, Rejected, outcome_rejected } +import v2.std.diagnostic { Accepted, Outcome, Rejected, outcome_rejected, port_locus } import v2.std.logic { Bool } import v2.std.algebra { Empty } import v2.std.node { Atom, Conj, Node, Symbol, TypeNode, SyntheticOccurrence } @@ -50,7 +50,7 @@ data rejecting_lens_authority_node: Node = Node { fn rejecting_lens_gate(_tree: InferredTree) -> Outcome> { outcome_rejected( - compile_lens_gate_rejected_diagnostic(at: PortLocus { port: ^rejecting_lens_gate_at }) + compile_lens_gate_rejected_diagnostic(at: port_locus(port: ^rejecting_lens_gate_at)) ) } diff --git a/src/v2/std/algebra.dag b/src/v2/std/algebra.dag index 1ae9863ac87..89daf5f33f7 100644 --- a/src/v2/std/algebra.dag +++ b/src/v2/std/algebra.dag @@ -725,6 +725,127 @@ fn list_snoc_item(xs: FreeMonoid, item: T) -> FreeMonoid { } +// Route C std de-fork PR-1 — FreeMonoid gap free-fns (additive; dsl record surface parity). +// 🟡 coproduct dissolution — feature:free-monoid-gap-free-fns — dissolve-on: dsl std/algebra FreeMonoid record deleted after PR-2 consumer migration. +type ListHeadResult + = HeadFound { value: T } + | HeadAbsent + +// v2 pair carrier for enumerate: dsl FreeMonoid.enumerate returns FreeMonoid>. +type IndexedElement { + index: Int + value: T +} + +// Endomorphic map: dsl FreeMonoid.map is fn(fn(T) -> T) -> FreeMonoid, not fn(T) -> U. +fn map(xs: FreeMonoid, f: fn(T) -> T) -> FreeMonoid { + fold_list_right(xs: xs, empty: Empty, snoc: fn(acc, item) { + Cons { head: f(item), tail: acc } + }) +} + +fn flat_map(xs: FreeMonoid, f: fn(T) -> FreeMonoid) -> FreeMonoid { + fold_list_right(xs: xs, empty: Empty, snoc: fn(acc, item) { + list_append(left: f(item), right: acc) + }) +} + +fn reverse(xs: FreeMonoid) -> FreeMonoid { + fold_list(xs: xs, empty: Empty, cons: fn(acc, item) { + Cons { head: item, tail: acc } + }) +} + +fn skip(xs: FreeMonoid, n: Int) -> FreeMonoid { + if n <= 0 { + xs + } else { + match xs { + Empty => Empty + Cons { head: _, tail: t } => skip(xs: t, n: n - 1) + } + } +} + +fn take(xs: FreeMonoid, n: Int) -> FreeMonoid { + if n <= 0 { + Empty + } else { + match xs { + Empty => Empty + Cons { head: h, tail: t } => Cons { head: h, tail: take(xs: t, n: n - 1) } + } + } +} + +fn slice(xs: FreeMonoid, start: Int, end: Int) -> FreeMonoid { + if end <= start { + Empty + } else { + take(xs: skip(xs: xs, n: start), n: end - start) + } +} + +fn list_insert_sorted_by(xs: FreeMonoid, item: T, cmp: fn(T, T) -> Int) -> FreeMonoid { + match xs { + Empty => Cons { head: item, tail: Empty } + Cons { head: h, tail: t } => + if cmp(item, h) <= 0 { + Cons { head: item, tail: xs } + } else { + Cons { head: h, tail: list_insert_sorted_by(xs: t, item: item, cmp: cmp) } + } + } +} + +fn sort_by(xs: FreeMonoid, cmp: fn(T, T) -> Int) -> FreeMonoid { + fold_list(xs: xs, empty: Empty, cons: fn(acc, item) { + list_insert_sorted_by(xs: acc, item: item, cmp: cmp) + }) +} + +fn first(xs: FreeMonoid) -> ListHeadResult { + match xs { + Empty => HeadAbsent + Cons { head: h, tail: _ } => HeadFound { value: h } + } +} + +fn last(xs: FreeMonoid) -> ListHeadResult { + match xs { + Empty => HeadAbsent + Cons { head: h, tail: t } => + match t { + Empty => HeadFound { value: h } + Cons { head: _, tail: _ } => last(xs: t) + } + } +} + +// Monoid-shaped fold: init plus step fn(T, T) -> T (left-to-right). Differs from fold_list's generic catamorphism. +fn fold(xs: FreeMonoid, init: T, step: fn(T, T) -> T) -> T { + fold_list(xs: xs, empty: init, cons: fn(acc, item) { step(acc, item) }) +} + +type EnumerateState { + index: Int + result: FreeMonoid> +} + +fn enumerate(xs: FreeMonoid) -> FreeMonoid> { + let state = fold_list(xs: xs, empty: EnumerateState { index: 0, result: Empty }, cons: fn(acc, item) { + EnumerateState { + index: acc.index + 1, + result: list_snoc_item( + xs: acc.result, + item: IndexedElement { index: acc.index, value: item } + ) + } + }) + state.result +} + + // Bag (multiset) equality: order-insensitive; equal lengths AND per-element // occurrence counts match. O(n^2) in the length of xs. fn bag_eq(xs: FreeMonoid, ys: FreeMonoid, eq: fn(T, T) -> Bool) -> Bool { diff --git a/src/v2/std/algebra_laws/freemonoid_gap_free_fns_test.dag b/src/v2/std/algebra_laws/freemonoid_gap_free_fns_test.dag new file mode 100644 index 00000000000..9ac25bdab93 --- /dev/null +++ b/src/v2/std/algebra_laws/freemonoid_gap_free_fns_test.dag @@ -0,0 +1,165 @@ +// Scope: execution witnesses for Route C Algebra PR-1 FreeMonoid gap free-fns. +// Status: load-bearing — each new std.algebra gap fn must stay green by execution. + +module v2.test.algebra_laws.freemonoid_gap_free_fns + +import v2.std.algebra { + Cons, + Empty, + Equal, + FreeMonoid, + Greater, + HeadAbsent, + HeadFound, + IndexedElement, + Less, + enumerate, + first, + flat_map, + fold, + last, + map, + reverse, + skip, + slice, + sort_by, + take, + zip_eq +} +import v2.std.integer { int_compare } +import v2.std.logic { Bool } +import v2.std.node { Atom, Node, Symbol, TypeNode, SyntheticOccurrence } + +fn gap_sym_eq(a: Symbol, b: Symbol) -> Bool { a == b } +fn gap_int_cmp(a: Int, b: Int) -> Int { + match int_compare(a: a, b: b) { + Less => -1 + Equal => 0 + Greater => 1 + } +} + +fn gap_sym_a() -> Symbol { ^gap_freemonoid_sym_a } +fn gap_sym_b() -> Symbol { ^gap_freemonoid_sym_b } +fn gap_sym_c() -> Symbol { ^gap_freemonoid_sym_c } + +fn gap_sym_ab() -> FreeMonoid { + Cons { head: gap_sym_a(), tail: Cons { head: gap_sym_b(), tail: Empty } } +} +fn gap_sym_abc() -> FreeMonoid { + Cons { + head: gap_sym_a(), + tail: Cons { head: gap_sym_b(), tail: Cons { head: gap_sym_c(), tail: Empty } } + } +} + +fn gap_map_identity_holds() -> Bool { + zip_eq( + a: map(xs: gap_sym_ab(), f: fn(x) { x }), + b: gap_sym_ab(), + eq: fn(x, y) { gap_sym_eq(a: x, b: y) } + ) +} + +fn gap_flat_map_singleton_holds() -> Bool { + zip_eq( + a: flat_map(xs: gap_sym_ab(), f: fn(x) { Cons { head: x, tail: Empty } }), + b: gap_sym_ab(), + eq: fn(x, y) { gap_sym_eq(a: x, b: y) } + ) +} + +fn gap_reverse_holds() -> Bool { + zip_eq( + a: reverse(xs: gap_sym_abc()), + b: Cons { + head: gap_sym_c(), + tail: Cons { head: gap_sym_b(), tail: Cons { head: gap_sym_a(), tail: Empty } } + }, + eq: fn(x, y) { gap_sym_eq(a: x, b: y) } + ) +} + +fn gap_skip_holds() -> Bool { + zip_eq( + a: skip(xs: gap_sym_abc(), n: 1), + b: Cons { head: gap_sym_b(), tail: Cons { head: gap_sym_c(), tail: Empty } }, + eq: fn(x, y) { gap_sym_eq(a: x, b: y) } + ) +} + +fn gap_take_holds() -> Bool { + zip_eq( + a: take(xs: gap_sym_abc(), n: 2), + b: gap_sym_ab(), + eq: fn(x, y) { gap_sym_eq(a: x, b: y) } + ) +} + +fn gap_slice_holds() -> Bool { + zip_eq( + a: slice(xs: gap_sym_abc(), start: 1, end: 3), + b: Cons { head: gap_sym_b(), tail: Cons { head: gap_sym_c(), tail: Empty } }, + eq: fn(x, y) { gap_sym_eq(a: x, b: y) } + ) +} + +fn gap_sort_by_holds() -> Bool { + zip_eq( + a: sort_by(xs: [3, 1, 2], cmp: fn(a, b) { gap_int_cmp(a: a, b: b) }), + b: [1, 2, 3], + eq: fn(a, b) { a == b } + ) +} + +fn gap_first_last_holds() -> Bool { + match first(xs: gap_sym_ab()) { + HeadFound { value: a } => + match last(xs: gap_sym_ab()) { + HeadFound { value: b } => + gap_sym_eq(a: a, b: gap_sym_a()) && gap_sym_eq(a: b, b: gap_sym_b()) + HeadAbsent => false + } + HeadAbsent => false + } +} + +fn gap_first_empty_holds() -> Bool { + match first(xs: Empty) { + HeadAbsent => true + HeadFound { value: _ } => false + } +} + +fn gap_fold_sum_holds() -> Bool { + fold(xs: [1, 2, 3], init: 0, step: fn(acc, item) { acc + item }) == 6 +} + +fn gap_enumerate_holds() -> Bool { + match enumerate(xs: gap_sym_ab()) { + Cons { + head: IndexedElement { index: i0, value: v0 }, + tail: Cons { + head: IndexedElement { index: i1, value: v1 }, + tail: Empty + } + } => + i0 == 0 + && i1 == 1 + && gap_sym_eq(a: v0, b: gap_sym_a()) + && gap_sym_eq(a: v1, b: gap_sym_b()) + _ => false + } +} + +test fn freemonoid_gap_map_identity_holds() -> Bool { gap_map_identity_holds() } +test fn freemonoid_gap_flat_map_singleton_holds() -> Bool { gap_flat_map_singleton_holds() } +test fn freemonoid_gap_reverse_holds() -> Bool { gap_reverse_holds() } +test fn freemonoid_gap_skip_holds() -> Bool { gap_skip_holds() } +test fn freemonoid_gap_take_holds() -> Bool { gap_take_holds() } +test fn freemonoid_gap_slice_holds() -> Bool { gap_slice_holds() } +test fn freemonoid_gap_sort_by_holds() -> Bool { gap_sort_by_holds() } +test fn freemonoid_gap_first_last_holds() -> Bool { gap_first_last_holds() } +test fn freemonoid_gap_first_empty_holds() -> Bool { gap_first_empty_holds() } +test fn freemonoid_gap_fold_sum_holds() -> Bool { gap_fold_sum_holds() } +test fn freemonoid_gap_enumerate_holds() -> Bool { gap_enumerate_holds() }