From 473d1ec3a5798c023e96c6fdec76765bcfe6e82d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 02:37:49 +0000 Subject: [PATCH 1/4] WIP: Track-A operation-grounding (cargo-green keystone): ground CanonicalOper --- ...del_canonical_operation_grounding_test.dag | 127 +++++++++++ src/v2/std/compilers/target_model.dag | 200 ++++++++++++++++-- 2 files changed, 313 insertions(+), 14 deletions(-) create mode 100644 src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag diff --git a/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag b/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag new file mode 100644 index 00000000000..a3707b64824 --- /dev/null +++ b/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag @@ -0,0 +1,127 @@ +module v2.test.manual.target_model_canonical_operation_grounding + +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.logic { Bool } +import v2.std.compilers.target_model { + CanonicalOperation, + InfixToken, + canonical_operation_op_add, + canonical_operation_op_sub, + canonical_operation_op_mul, + canonical_operation_op_div, + canonical_operation_op_and, + canonical_operation_op_or, + canonical_operation_op_not, + canonical_operation_op_less, + canonical_operation_op_less_or_equal, + canonical_operation_op_greater, + canonical_operation_op_greater_or_equal, + canonical_operation_op_equal, + canonical_operation_op_not_equal, + canonical_operation_equal, + canonical_operation_from_wire_node, + target_model_canonical_operation_wire_node, + target_operator_realization_catalog_lookup, + target_operator_realization_node, + target_operator_realizations_catalog_node +} + +fn op_round_trips(op: CanonicalOperation) -> Bool { + match canonical_operation_from_wire_node( + wire: target_model_canonical_operation_wire_node(operation: op) + ) { + Accepted { value: decoded, diagnostics: _ } => + canonical_operation_equal(left: decoded, right: op) + Rejected { diagnostics: _ } => false + } +} + +fn ops_distinct(left: CanonicalOperation, right: CanonicalOperation) -> Bool { + match canonical_operation_equal(left: left, right: right) { + true => false + false => true + } +} + +fn mul_only_catalog() -> Node { + target_operator_realizations_catalog_node( + rows: [ + target_operator_realization_node( + operation: canonical_operation_op_mul(), + shape: InfixToken { token: ^rust_token_star } + ) + ] + ) +} + +test fn arith_ops_round_trip() -> Bool { + op_round_trips(op: canonical_operation_op_add()) && + op_round_trips(op: canonical_operation_op_sub()) && + op_round_trips(op: canonical_operation_op_mul()) && + op_round_trips(op: canonical_operation_op_div()) +} + +test fn boolean_ops_round_trip() -> Bool { + op_round_trips(op: canonical_operation_op_and()) && + op_round_trips(op: canonical_operation_op_or()) && + op_round_trips(op: canonical_operation_op_not()) +} + +test fn comparison_ops_round_trip() -> Bool { + op_round_trips(op: canonical_operation_op_less()) && + op_round_trips(op: canonical_operation_op_less_or_equal()) && + op_round_trips(op: canonical_operation_op_greater()) && + op_round_trips(op: canonical_operation_op_greater_or_equal()) && + op_round_trips(op: canonical_operation_op_equal()) && + op_round_trips(op: canonical_operation_op_not_equal()) +} + +test fn distinct_algebra_fields_discriminate() -> Bool { + ops_distinct(left: canonical_operation_op_add(), right: canonical_operation_op_sub()) && + ops_distinct(left: canonical_operation_op_add(), right: canonical_operation_op_mul()) && + ops_distinct(left: canonical_operation_op_mul(), right: canonical_operation_op_div()) && + ops_distinct(left: canonical_operation_op_and(), right: canonical_operation_op_or()) +} + +test fn shared_compare_field_relations_discriminate() -> Bool { + ops_distinct(left: canonical_operation_op_less(), right: canonical_operation_op_less_or_equal()) && + ops_distinct(left: canonical_operation_op_less(), right: canonical_operation_op_greater()) && + ops_distinct(left: canonical_operation_op_equal(), right: canonical_operation_op_not_equal()) && + ops_distinct(left: canonical_operation_op_greater(), right: canonical_operation_op_greater_or_equal()) +} + +test fn cross_family_ops_discriminate() -> Bool { + ops_distinct(left: canonical_operation_op_add(), right: canonical_operation_op_less()) && + ops_distinct(left: canonical_operation_op_equal(), right: canonical_operation_op_add()) +} + +test fn same_op_is_equal() -> Bool { + canonical_operation_equal( + left: canonical_operation_op_less_or_equal(), + right: canonical_operation_op_less_or_equal() + ) && + canonical_operation_equal( + left: canonical_operation_op_sub(), + right: canonical_operation_op_sub() + ) +} + +test fn catalog_lookup_accepts_grounded_op() -> Bool { + match target_operator_realization_catalog_lookup( + catalog: mul_only_catalog(), + canonical_op: canonical_operation_op_mul() + ) { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +test fn catalog_lookup_misses_absent_op() -> Bool { + match target_operator_realization_catalog_lookup( + catalog: mul_only_catalog(), + canonical_op: canonical_operation_op_add() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index 9a0515ed0bf..f8ccf138fbc 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -546,11 +546,115 @@ type TargetValueTemplate { node: Node } +type CanonicalOrderRelation + = OrderLess + | OrderLessOrEqual + | OrderGreater + | OrderGreaterOrEqual + | OrderEqual + | OrderNotEqual + type CanonicalOperation - = OpAdd { algebra_field: Symbol } + = AlgebraFieldOperation { algebra_field: Symbol } + | OrderRelationOperation { compare_field: Symbol, relation: CanonicalOrderRelation } fn canonical_operation_op_add() -> CanonicalOperation { - OpAdd { algebra_field: ^ring_field_add } + AlgebraFieldOperation { algebra_field: ^ring_field_add } +} + +fn canonical_operation_op_sub() -> CanonicalOperation { + AlgebraFieldOperation { algebra_field: ^group_field_inverse } +} + +fn canonical_operation_op_mul() -> CanonicalOperation { + AlgebraFieldOperation { algebra_field: ^ring_field_mul } +} + +fn canonical_operation_op_div() -> CanonicalOperation { + AlgebraFieldOperation { algebra_field: ^field_field_reciprocal } +} + +fn canonical_operation_op_and() -> CanonicalOperation { + AlgebraFieldOperation { algebra_field: ^lattice_field_meet } +} + +fn canonical_operation_op_or() -> CanonicalOperation { + AlgebraFieldOperation { algebra_field: ^lattice_field_join } +} + +fn canonical_operation_op_not() -> CanonicalOperation { + AlgebraFieldOperation { algebra_field: ^boolean_algebra_field_complement } +} + +fn canonical_operation_op_less() -> CanonicalOperation { + OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderLess } +} + +fn canonical_operation_op_less_or_equal() -> CanonicalOperation { + OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderLessOrEqual } +} + +fn canonical_operation_op_greater() -> CanonicalOperation { + OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderGreater } +} + +fn canonical_operation_op_greater_or_equal() -> CanonicalOperation { + OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderGreaterOrEqual } +} + +fn canonical_operation_op_equal() -> CanonicalOperation { + OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderEqual } +} + +fn canonical_operation_op_not_equal() -> CanonicalOperation { + OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderNotEqual } +} + +fn canonical_order_relation_symbol(relation: CanonicalOrderRelation) -> Symbol { + match relation { + OrderLess => discriminant(v: OrderLess) + OrderLessOrEqual => discriminant(v: OrderLessOrEqual) + OrderGreater => discriminant(v: OrderGreater) + OrderGreaterOrEqual => discriminant(v: OrderGreaterOrEqual) + OrderEqual => discriminant(v: OrderEqual) + OrderNotEqual => discriminant(v: OrderNotEqual) + } +} + +fn canonical_order_relation_from_symbol(id: Symbol) -> Optional { + if id == discriminant(v: OrderLess) { + optional_present(value: OrderLess) + } else { + if id == discriminant(v: OrderLessOrEqual) { + optional_present(value: OrderLessOrEqual) + } else { + if id == discriminant(v: OrderGreater) { + optional_present(value: OrderGreater) + } else { + if id == discriminant(v: OrderGreaterOrEqual) { + optional_present(value: OrderGreaterOrEqual) + } else { + if id == discriminant(v: OrderEqual) { + optional_present(value: OrderEqual) + } else { + if id == discriminant(v: OrderNotEqual) { + optional_present(value: OrderNotEqual) + } else { + optional_absent() + } + } + } + } + } + } +} + +fn canonical_order_relation_equal( + left: CanonicalOrderRelation, + right: CanonicalOrderRelation +) -> Bool { + canonical_order_relation_symbol(relation: left) + == canonical_order_relation_symbol(relation: right) } type TargetOperatorShape @@ -681,7 +785,10 @@ fn target_canonical_operation_wire_malformed_diagnostic(wire: Node) -> Diagnosti } } -fn target_model_canonical_operation_algebra_field_from_wire(wire: Node) -> Optional { +fn target_model_canonical_operation_field_symbol_from_wire( + wire: Node, + field_name: Symbol +) -> Optional { match fold( wire.children, init: optional_absent(), @@ -691,7 +798,7 @@ fn target_model_canonical_operation_algebra_field_from_wire(wire: Node) -> Optio Absent => match edge.label { Named { name: n } => - if n == ^target_canonical_operation_field_algebra_field { + if n == field_name { match edge.target.kind { TypeNode { connective: Atom { identity: id } } => optional_present(value: id) @@ -710,11 +817,23 @@ fn target_model_canonical_operation_algebra_field_from_wire(wire: Node) -> Optio } } +fn target_model_canonical_operation_relation_from_wire( + wire: Node +) -> Optional { + match target_model_canonical_operation_field_symbol_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_relation + ) { + Present { value: id } => canonical_order_relation_from_symbol(id: id) + Absent => optional_absent() + } +} + fn target_model_canonical_operation_wire_node(operation: CanonicalOperation) -> Node { match operation { - OpAdd { algebra_field: f } => + AlgebraFieldOperation { algebra_field: f } => Node { - kind: TypeNode { connective: Atom { identity: discriminant(v: OpAdd {}) } }, + kind: TypeNode { connective: Atom { identity: discriminant(v: AlgebraFieldOperation {}) } }, children: [ target_model_named_edge( name: ^target_canonical_operation_field_algebra_field, @@ -723,6 +842,23 @@ fn target_model_canonical_operation_wire_node(operation: CanonicalOperation) -> ], occurrence_id: SyntheticOccurrence } + OrderRelationOperation { compare_field: cf, relation: r } => + Node { + kind: TypeNode { connective: Atom { identity: discriminant(v: OrderRelationOperation {}) } }, + children: [ + target_model_named_edge( + name: ^target_canonical_operation_field_compare_field, + target: target_model_type_atom_node(identity: cf) + ), + target_model_named_edge( + name: ^target_canonical_operation_field_relation, + target: target_model_type_atom_node( + identity: canonical_order_relation_symbol(relation: r) + ) + ) + ], + occurrence_id: SyntheticOccurrence + } } } @@ -731,9 +867,16 @@ fn canonical_operation_equal( right: CanonicalOperation ) -> Bool { match left { - OpAdd { algebra_field: lf } => + AlgebraFieldOperation { algebra_field: lf } => match right { - OpAdd { algebra_field: rf } => lf == rf + AlgebraFieldOperation { algebra_field: rf } => lf == rf + OrderRelationOperation { compare_field: _, relation: _ } => false + } + OrderRelationOperation { compare_field: lcf, relation: lr } => + match right { + AlgebraFieldOperation { algebra_field: _ } => false + OrderRelationOperation { compare_field: rcf, relation: rr } => + lcf == rcf && canonical_order_relation_equal(left: lr, right: rr) } } } @@ -741,19 +884,48 @@ fn canonical_operation_equal( fn canonical_operation_from_wire_node(wire: Node) -> Outcome { match wire.kind { TypeNode { connective: Atom { identity: id } } => - if id == discriminant(v: OpAdd {}) { - match target_model_canonical_operation_algebra_field_from_wire(wire: wire) { + if id == discriminant(v: AlgebraFieldOperation {}) { + match target_model_canonical_operation_field_symbol_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_algebra_field + ) { Present { value: algebra_field } => - outcome_accepted(OpAdd { algebra_field: algebra_field }) + outcome_accepted(AlgebraFieldOperation { algebra_field: algebra_field }) Absent => outcome_rejected( target_canonical_operation_wire_malformed_diagnostic(wire: wire) ) } } else { - outcome_rejected( - target_canonical_operation_wire_malformed_diagnostic(wire: wire) - ) + if id == discriminant(v: OrderRelationOperation {}) { + match target_model_canonical_operation_field_symbol_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_compare_field + ) { + Present { value: compare_field } => + match target_model_canonical_operation_relation_from_wire(wire: wire) { + Present { value: relation } => + outcome_accepted( + OrderRelationOperation { + compare_field: compare_field, + relation: relation + } + ) + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + } else { + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } } _ => outcome_rejected( From df6cc310182f6343eac1c0bed0e82967ea9ecf33 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 02:51:48 +0000 Subject: [PATCH 2/4] WIP: Track-A operation-grounding (cargo-green keystone): ground CanonicalOper --- src/v1/tests/src/lib.rs | 2 + .../zz_temp_canonical_op_grounding_test.rs | 50 +++++++++++++++++++ ...del_canonical_operation_grounding_test.dag | 1 + src/v2/std/compilers/target_model.dag | 3 +- 4 files changed, 54 insertions(+), 2 deletions(-) create mode 100644 src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs diff --git a/src/v1/tests/src/lib.rs b/src/v1/tests/src/lib.rs index d34fe11631a..d11004c30a1 100644 --- a/src/v1/tests/src/lib.rs +++ b/src/v1/tests/src/lib.rs @@ -132,3 +132,5 @@ mod wet_hermetic_equivalence_test; mod width_nat_type_arg_test; #[cfg(test)] mod witness_option_bridge_test; +#[cfg(test)] +mod zz_temp_canonical_op_grounding_test; diff --git a/src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs b/src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs new file mode 100644 index 00000000000..4e5b86978ee --- /dev/null +++ b/src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs @@ -0,0 +1,50 @@ +use std::rc::Rc; + +use v1_compiler::cli_run; +use v1_compiler::v1_compiler_compile::compile_to_resolved; +use v1_compiler::v1_interpreter::{self, ExecutionMode, Value}; +use v1_compiler::v1_std_core::diagnostic_to_message; + +use crate::helpers::{v2_layer_roots, workspace_root}; + +const TEST_FNS: &[&str] = &[ + "arith_ops_round_trip", + "boolean_ops_round_trip", + "comparison_ops_round_trip", + "distinct_algebra_fields_discriminate", + "shared_compare_field_relations_discriminate", + "cross_family_ops_discriminate", + "same_op_is_equal", + "catalog_lookup_accepts_grounded_op", + "catalog_lookup_misses_absent_op", +]; + +#[test] +fn canonical_operation_grounding_witnesses_run_green() { + let roots: Vec = v2_layer_roots() + .iter() + .map(|p| p.to_string_lossy().to_string()) + .collect(); + let entry = workspace_root() + .join("src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag"); + let entry = entry.to_string_lossy().to_string(); + let sources = cli_run::load_sources_for_entry(&roots, &entry) + .unwrap_or_else(|e| panic!("failed to load {entry}: {e}")); + let resolved = compile_to_resolved(Rc::new(sources)); + let msgs: Vec = resolved + .diagnostics + .iter() + .map(|d| diagnostic_to_message(d.diagnostic.clone())) + .filter(|m| !m.starts_with("complexity: ")) + .collect(); + assert!(msgs.is_empty(), "witness corpus should resolve: {msgs:?}"); + let graph = resolved.graph.as_ref().expect("graph"); + let ctx = + cli_run::make_eval_context(graph, resolved.source_indices.clone(), ExecutionMode::Wet); + for f in TEST_FNS { + match v1_interpreter::run_in_context(&ctx, f, false) { + Ok(Value::Bool(true)) => {} + other => panic!("{f} expected Bool(true), got {other:?}"), + } + } +} diff --git a/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag b/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag index a3707b64824..16b36fe5d8a 100644 --- a/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag +++ b/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag @@ -2,6 +2,7 @@ module v2.test.manual.target_model_canonical_operation_grounding import v2.std.diagnostic { Accepted, Rejected } import v2.std.logic { Bool } +import v2.std.node { Node } import v2.std.compilers.target_model { CanonicalOperation, InfixToken, diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index f8ccf138fbc..b497f20fd8e 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -653,8 +653,7 @@ fn canonical_order_relation_equal( left: CanonicalOrderRelation, right: CanonicalOrderRelation ) -> Bool { - canonical_order_relation_symbol(relation: left) - == canonical_order_relation_symbol(relation: right) + canonical_order_relation_symbol(relation: left) == canonical_order_relation_symbol(relation: right) } type TargetOperatorShape From ba5bea550babd18cea67530b0cb48d3b57b857db Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 02:52:30 +0000 Subject: [PATCH 3/4] Remove local-only temp rust witness harness (the .dag witness is auto-enrolled in the CI floor) Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v1/tests/src/lib.rs | 2 - .../zz_temp_canonical_op_grounding_test.rs | 50 ------------------- 2 files changed, 52 deletions(-) delete mode 100644 src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs diff --git a/src/v1/tests/src/lib.rs b/src/v1/tests/src/lib.rs index d11004c30a1..d34fe11631a 100644 --- a/src/v1/tests/src/lib.rs +++ b/src/v1/tests/src/lib.rs @@ -132,5 +132,3 @@ mod wet_hermetic_equivalence_test; mod width_nat_type_arg_test; #[cfg(test)] mod witness_option_bridge_test; -#[cfg(test)] -mod zz_temp_canonical_op_grounding_test; diff --git a/src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs b/src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs deleted file mode 100644 index 4e5b86978ee..00000000000 --- a/src/v1/tests/src/zz_temp_canonical_op_grounding_test.rs +++ /dev/null @@ -1,50 +0,0 @@ -use std::rc::Rc; - -use v1_compiler::cli_run; -use v1_compiler::v1_compiler_compile::compile_to_resolved; -use v1_compiler::v1_interpreter::{self, ExecutionMode, Value}; -use v1_compiler::v1_std_core::diagnostic_to_message; - -use crate::helpers::{v2_layer_roots, workspace_root}; - -const TEST_FNS: &[&str] = &[ - "arith_ops_round_trip", - "boolean_ops_round_trip", - "comparison_ops_round_trip", - "distinct_algebra_fields_discriminate", - "shared_compare_field_relations_discriminate", - "cross_family_ops_discriminate", - "same_op_is_equal", - "catalog_lookup_accepts_grounded_op", - "catalog_lookup_misses_absent_op", -]; - -#[test] -fn canonical_operation_grounding_witnesses_run_green() { - let roots: Vec = v2_layer_roots() - .iter() - .map(|p| p.to_string_lossy().to_string()) - .collect(); - let entry = workspace_root() - .join("src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag"); - let entry = entry.to_string_lossy().to_string(); - let sources = cli_run::load_sources_for_entry(&roots, &entry) - .unwrap_or_else(|e| panic!("failed to load {entry}: {e}")); - let resolved = compile_to_resolved(Rc::new(sources)); - let msgs: Vec = resolved - .diagnostics - .iter() - .map(|d| diagnostic_to_message(d.diagnostic.clone())) - .filter(|m| !m.starts_with("complexity: ")) - .collect(); - assert!(msgs.is_empty(), "witness corpus should resolve: {msgs:?}"); - let graph = resolved.graph.as_ref().expect("graph"); - let ctx = - cli_run::make_eval_context(graph, resolved.source_indices.clone(), ExecutionMode::Wet); - for f in TEST_FNS { - match v1_interpreter::run_in_context(&ctx, f, false) { - Ok(Value::Bool(true)) => {} - other => panic!("{f} expected Bool(true), got {other:?}"), - } - } -} From d9aeae92221e28f999ac2166d48c66d0b7900a42 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 03:22:36 +0000 Subject: [PATCH 4/4] Restore full Track-A scope: 4-variant CanonicalOperation + Equivalence mint, exhaustive (lens-green) equal Co-Authored-By: Claude Opus 4.8 (1M context) --- ...del_canonical_operation_grounding_test.dag | 128 ------ ...eration_grounding_emit_typescript_test.dag | 235 +++++++++++ src/v2/std/algebra.dag | 35 ++ src/v2/std/compilers/target_model.dag | 383 ++++++++++++------ 4 files changed, 539 insertions(+), 242 deletions(-) delete mode 100644 src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag create mode 100644 src/v2/compiler/manual/target_operation_grounding_emit_typescript_test.dag diff --git a/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag b/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag deleted file mode 100644 index 16b36fe5d8a..00000000000 --- a/src/v2/compiler/manual/target_model_canonical_operation_grounding_test.dag +++ /dev/null @@ -1,128 +0,0 @@ -module v2.test.manual.target_model_canonical_operation_grounding - -import v2.std.diagnostic { Accepted, Rejected } -import v2.std.logic { Bool } -import v2.std.node { Node } -import v2.std.compilers.target_model { - CanonicalOperation, - InfixToken, - canonical_operation_op_add, - canonical_operation_op_sub, - canonical_operation_op_mul, - canonical_operation_op_div, - canonical_operation_op_and, - canonical_operation_op_or, - canonical_operation_op_not, - canonical_operation_op_less, - canonical_operation_op_less_or_equal, - canonical_operation_op_greater, - canonical_operation_op_greater_or_equal, - canonical_operation_op_equal, - canonical_operation_op_not_equal, - canonical_operation_equal, - canonical_operation_from_wire_node, - target_model_canonical_operation_wire_node, - target_operator_realization_catalog_lookup, - target_operator_realization_node, - target_operator_realizations_catalog_node -} - -fn op_round_trips(op: CanonicalOperation) -> Bool { - match canonical_operation_from_wire_node( - wire: target_model_canonical_operation_wire_node(operation: op) - ) { - Accepted { value: decoded, diagnostics: _ } => - canonical_operation_equal(left: decoded, right: op) - Rejected { diagnostics: _ } => false - } -} - -fn ops_distinct(left: CanonicalOperation, right: CanonicalOperation) -> Bool { - match canonical_operation_equal(left: left, right: right) { - true => false - false => true - } -} - -fn mul_only_catalog() -> Node { - target_operator_realizations_catalog_node( - rows: [ - target_operator_realization_node( - operation: canonical_operation_op_mul(), - shape: InfixToken { token: ^rust_token_star } - ) - ] - ) -} - -test fn arith_ops_round_trip() -> Bool { - op_round_trips(op: canonical_operation_op_add()) && - op_round_trips(op: canonical_operation_op_sub()) && - op_round_trips(op: canonical_operation_op_mul()) && - op_round_trips(op: canonical_operation_op_div()) -} - -test fn boolean_ops_round_trip() -> Bool { - op_round_trips(op: canonical_operation_op_and()) && - op_round_trips(op: canonical_operation_op_or()) && - op_round_trips(op: canonical_operation_op_not()) -} - -test fn comparison_ops_round_trip() -> Bool { - op_round_trips(op: canonical_operation_op_less()) && - op_round_trips(op: canonical_operation_op_less_or_equal()) && - op_round_trips(op: canonical_operation_op_greater()) && - op_round_trips(op: canonical_operation_op_greater_or_equal()) && - op_round_trips(op: canonical_operation_op_equal()) && - op_round_trips(op: canonical_operation_op_not_equal()) -} - -test fn distinct_algebra_fields_discriminate() -> Bool { - ops_distinct(left: canonical_operation_op_add(), right: canonical_operation_op_sub()) && - ops_distinct(left: canonical_operation_op_add(), right: canonical_operation_op_mul()) && - ops_distinct(left: canonical_operation_op_mul(), right: canonical_operation_op_div()) && - ops_distinct(left: canonical_operation_op_and(), right: canonical_operation_op_or()) -} - -test fn shared_compare_field_relations_discriminate() -> Bool { - ops_distinct(left: canonical_operation_op_less(), right: canonical_operation_op_less_or_equal()) && - ops_distinct(left: canonical_operation_op_less(), right: canonical_operation_op_greater()) && - ops_distinct(left: canonical_operation_op_equal(), right: canonical_operation_op_not_equal()) && - ops_distinct(left: canonical_operation_op_greater(), right: canonical_operation_op_greater_or_equal()) -} - -test fn cross_family_ops_discriminate() -> Bool { - ops_distinct(left: canonical_operation_op_add(), right: canonical_operation_op_less()) && - ops_distinct(left: canonical_operation_op_equal(), right: canonical_operation_op_add()) -} - -test fn same_op_is_equal() -> Bool { - canonical_operation_equal( - left: canonical_operation_op_less_or_equal(), - right: canonical_operation_op_less_or_equal() - ) && - canonical_operation_equal( - left: canonical_operation_op_sub(), - right: canonical_operation_op_sub() - ) -} - -test fn catalog_lookup_accepts_grounded_op() -> Bool { - match target_operator_realization_catalog_lookup( - catalog: mul_only_catalog(), - canonical_op: canonical_operation_op_mul() - ) { - Accepted { value: _, diagnostics: _ } => true - Rejected { diagnostics: _ } => false - } -} - -test fn catalog_lookup_misses_absent_op() -> Bool { - match target_operator_realization_catalog_lookup( - catalog: mul_only_catalog(), - canonical_op: canonical_operation_op_add() - ) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: _ } => true - } -} diff --git a/src/v2/compiler/manual/target_operation_grounding_emit_typescript_test.dag b/src/v2/compiler/manual/target_operation_grounding_emit_typescript_test.dag new file mode 100644 index 00000000000..ebdda66cbdb --- /dev/null +++ b/src/v2/compiler/manual/target_operation_grounding_emit_typescript_test.dag @@ -0,0 +1,235 @@ +module v2.test.manual.target_operation_grounding_emit_typescript + +import v2.std.compilers.target_model { + CanonicalOperation, + InfixToken, + IsLess, + IsLessOrEqual, + IsGreater, + IsGreaterOrEqual, + IsEqual, + IsNotEqual, + TargetModel, + TargetValueExpression, + canonical_operation_op_add, + canonical_operation_op_sub, + canonical_operation_op_mul, + canonical_operation_op_div, + canonical_operation_op_negate, + canonical_operation_op_and, + canonical_operation_op_or, + canonical_operation_op_not, + canonical_operation_op_lt, + canonical_operation_op_le, + canonical_operation_op_gt, + canonical_operation_op_ge, + canonical_operation_op_eq, + canonical_operation_op_ne, + canonical_operation_wire_matches_operation, + equality_predicate_accepts, + ordering_predicate_accepts, + target_model_canonical_operation_wire_node, + target_model_emit_transforms_empty, + target_operator_realization_node, + target_operator_realizations_catalog_node, + target_value_expression_binding_ref, + target_value_expression_primitive_apply, + target_value_expression_primitive_apply_to_concrete_tokens +} +import v2.compiler.translate { serialize_concrete_syntax_tokens_to_source_string } +import v2.extdeps.languages.typescript { + ts_lex_rule, + ts_mvp1_binding_spellings, + ts_value_expression_projection +} +import v2.std.compilers.lexing { LexRuleSet, LexRules, ModeledLexRules } +import v2.std.collection { List } +import v2.std.algebra { Equal, Greater, Less, Ordering, zip_eq } +import v2.std.diagnostic { Accepted, Outcome, Rejected, bind_outcome } +import v2.std.host_transport { target_emit_host_runtime_row_unconfigured } +import v2.std.logic { Bool } +import v2.std.node { Conj, Node, Symbol, SyntheticOccurrence, TypeNode } + +fn op_grounding_test_lex() -> LexRules { + ModeledLexRules { + root: LexRuleSet { + rules: [ + ts_lex_rule(token_class: ^op_grounding_token_plus, text: " + "), + ts_lex_rule(token_class: ^op_grounding_token_minus, text: " - "), + ts_lex_rule(token_class: ^op_grounding_token_lt, text: " < "), + ts_lex_rule(token_class: ^op_grounding_token_eqeq, text: " == ") + ] + } + } +} + +fn op_grounding_test_bundle() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + } +} + +fn op_grounding_test_model() -> TargetModel { + TargetModel { + bundle: op_grounding_test_bundle(), + lex: op_grounding_test_lex(), + binding_spellings: ts_mvp1_binding_spellings(), + token_class_emit_transforms: target_model_emit_transforms_empty, + authority_source_text: "", + runtime_row: target_emit_host_runtime_row_unconfigured + } +} + +fn op_grounding_realization_row(operation: CanonicalOperation, token: Symbol) -> Node { + target_operator_realization_node( + operation: operation, + shape: InfixToken { token: token } + ) +} + +fn op_grounding_catalog() -> Node { + target_operator_realizations_catalog_node( + rows: [ + op_grounding_realization_row(operation: canonical_operation_op_sub(), token: ^op_grounding_token_minus), + op_grounding_realization_row(operation: canonical_operation_op_lt(), token: ^op_grounding_token_lt), + op_grounding_realization_row(operation: canonical_operation_op_eq(), token: ^op_grounding_token_eqeq) + ] + ) +} + +fn op_grounding_catalog_sub_mistoken() -> Node { + target_operator_realizations_catalog_node( + rows: [ + op_grounding_realization_row(operation: canonical_operation_op_sub(), token: ^op_grounding_token_plus) + ] + ) +} + +fn op_grounding_catalog_sub_only() -> Node { + target_operator_realizations_catalog_node( + rows: [ + op_grounding_realization_row(operation: canonical_operation_op_sub(), token: ^op_grounding_token_minus) + ] + ) +} + +fn op_grounding_binary_expr(operation: CanonicalOperation) -> TargetValueExpression { + target_value_expression_primitive_apply( + operation: operation, + operands: [ + target_value_expression_binding_ref(binding: ^ts_binding_param_x), + target_value_expression_binding_ref(binding: ^ts_binding_param_y) + ] + ) +} + +fn op_grounding_emit(operation: CanonicalOperation, catalog: Node) -> Outcome { + bind_outcome( + o: target_value_expression_primitive_apply_to_concrete_tokens( + expr: op_grounding_binary_expr(operation: operation), + projection: ts_value_expression_projection(), + catalog: catalog + ), + f: fn(tokens) { + serialize_concrete_syntax_tokens_to_source_string( + target: op_grounding_test_model(), + tokens: tokens + ) + } + ) +} + +test fn op_grounding_emits_subtraction() -> Bool { + match op_grounding_emit(operation: canonical_operation_op_sub(), catalog: op_grounding_catalog()) { + Accepted { value: s, diagnostics: _ } => s == "x - y" + Rejected { diagnostics: _ } => false + } +} + +test fn op_grounding_emits_less_than() -> Bool { + match op_grounding_emit(operation: canonical_operation_op_lt(), catalog: op_grounding_catalog()) { + Accepted { value: s, diagnostics: _ } => s == "x < y" + Rejected { diagnostics: _ } => false + } +} + +test fn op_grounding_emits_equality() -> Bool { + match op_grounding_emit(operation: canonical_operation_op_eq(), catalog: op_grounding_catalog()) { + Accepted { value: s, diagnostics: _ } => s == "x == y" + Rejected { diagnostics: _ } => false + } +} + +test fn op_grounding_wrong_token_discriminates() -> Bool { + match op_grounding_emit(operation: canonical_operation_op_sub(), catalog: op_grounding_catalog_sub_mistoken()) { + Accepted { value: s, diagnostics: _ } => (s == "x + y") && (s != "x - y") + Rejected { diagnostics: _ } => false + } +} + +test fn op_grounding_catalog_miss_rejects() -> Bool { + match op_grounding_emit(operation: canonical_operation_op_lt(), catalog: op_grounding_catalog_sub_only()) { + Rejected { diagnostics: _ } => true + Accepted { value: _, diagnostics: _ } => false + } +} + +fn op_grounding_wire_roundtrips(operation: CanonicalOperation) -> Bool { + canonical_operation_wire_matches_operation( + wire: target_model_canonical_operation_wire_node(operation: operation), + operation: operation + ) +} + +test fn op_grounding_wire_roundtrips_all() -> Bool { + op_grounding_wire_roundtrips(operation: canonical_operation_op_add()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_sub()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_mul()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_div()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_negate()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_and()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_or()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_not()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_lt()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_le()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_gt()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_ge()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_eq()) && + op_grounding_wire_roundtrips(operation: canonical_operation_op_ne()) +} + +fn op_grounding_wire_rejects(produced: CanonicalOperation, probed: CanonicalOperation) -> Bool { + canonical_operation_wire_matches_operation( + wire: target_model_canonical_operation_wire_node(operation: produced), + operation: probed + ) +} + +test fn op_grounding_wire_discriminates() -> Bool { + !op_grounding_wire_rejects(produced: canonical_operation_op_sub(), probed: canonical_operation_op_add()) && + !op_grounding_wire_rejects(produced: canonical_operation_op_lt(), probed: canonical_operation_op_gt()) && + !op_grounding_wire_rejects(produced: canonical_operation_op_le(), probed: canonical_operation_op_ge()) && + !op_grounding_wire_rejects(produced: canonical_operation_op_eq(), probed: canonical_operation_op_ne()) +} + +fn op_grounding_ordering_eq(a: Ordering, b: Ordering) -> Bool { + discriminant(v: a) == discriminant(v: b) +} + +fn op_grounding_ordering_list_eq(left: List, right: List) -> Bool { + zip_eq(a: left, b: right, eq: fn(x, y) { op_grounding_ordering_eq(a: x, b: y) }) +} + +test fn op_grounding_ordering_predicate_accepts_units() -> Bool { + op_grounding_ordering_list_eq(left: ordering_predicate_accepts(predicate: IsLess), right: [Less]) && + op_grounding_ordering_list_eq(left: ordering_predicate_accepts(predicate: IsLessOrEqual), right: [Less, Equal]) && + op_grounding_ordering_list_eq(left: ordering_predicate_accepts(predicate: IsGreater), right: [Greater]) && + op_grounding_ordering_list_eq(left: ordering_predicate_accepts(predicate: IsGreaterOrEqual), right: [Equal, Greater]) +} + +test fn op_grounding_equality_predicate_accepts_units() -> Bool { + (equality_predicate_accepts(predicate: IsEqual) == true) && + (equality_predicate_accepts(predicate: IsNotEqual) == false) +} diff --git a/src/v2/std/algebra.dag b/src/v2/std/algebra.dag index 3f3533ee488..1d3b4cfed60 100644 --- a/src/v2/std/algebra.dag +++ b/src/v2/std/algebra.dag @@ -66,6 +66,10 @@ type BooleanAlgebra { complement: fn(T) -> T } +type Equivalence { + eq: fn(T, T) -> Bool +} + type FreeMonoid = Empty | Cons { head: T, tail: FreeMonoid } @@ -579,6 +583,37 @@ fn boolean_algebra_node(inhabitant: Node) -> Node { ) } +fn bool_type_node() -> Node { + Node { + kind: TypeNode { connective: Disj }, + children: [ + Edge { label: Named { name: ^bool_variant_true }, target: algebra_empty_conj() }, + Edge { label: Named { name: ^bool_variant_false }, target: algebra_empty_conj() }, + ], + occurrence_id: SyntheticOccurrence +} +} + +fn equivalence_type_node(inhabitant: Node) -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: ^equivalence_field_eq }, + target: algebra_binary_fn_node(domain: inhabitant, codomain: bool_type_node()) + }, + ], + occurrence_id: SyntheticOccurrence +} +} + +fn equivalence_node(inhabitant: Node) -> Node { + algebra_inhabitance_node( + algebra: equivalence_type_node(inhabitant: inhabitant), + inhabitant: inhabitant + ) +} + fn free_monoid_node(inhabitant: Node) -> Node { algebra_inhabitance_node( algebra: free_monoid_type_node(inhabitant: inhabitant), diff --git a/src/v2/std/compilers/target_model.dag b/src/v2/std/compilers/target_model.dag index b497f20fd8e..6dfe547a6ec 100644 --- a/src/v2/std/compilers/target_model.dag +++ b/src/v2/std/compilers/target_model.dag @@ -3,6 +3,10 @@ module v2.std.compilers.target_model import v2.std.algebra { Cons, Empty, + Equal, + Greater, + Less, + Ordering, FreeMonoid, fold_list, fold_list_node, @@ -546,114 +550,98 @@ type TargetValueTemplate { node: Node } -type CanonicalOrderRelation - = OrderLess - | OrderLessOrEqual - | OrderGreater - | OrderGreaterOrEqual - | OrderEqual - | OrderNotEqual +type OrderingPredicate + = IsLess + | IsLessOrEqual + | IsGreater + | IsGreaterOrEqual + +type EqualityPredicate + = IsEqual + | IsNotEqual type CanonicalOperation - = AlgebraFieldOperation { algebra_field: Symbol } - | OrderRelationOperation { compare_field: Symbol, relation: CanonicalOrderRelation } + = AlgebraPrimitive { algebra_field: Symbol } + | AlgebraInverseCompose { binary_field: Symbol, inverse_field: Symbol } + | OrderingComparison { compare_field: Symbol, predicate: OrderingPredicate } + | EqualityComparison { eq_field: Symbol, predicate: EqualityPredicate } -fn canonical_operation_op_add() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^ring_field_add } +fn ordering_predicate_accepts(predicate: OrderingPredicate) -> List { + match predicate { + IsLess => [Less] + IsLessOrEqual => [Less, Equal] + IsGreater => [Greater] + IsGreaterOrEqual => [Equal, Greater] + } } -fn canonical_operation_op_sub() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^group_field_inverse } +fn equality_predicate_accepts(predicate: EqualityPredicate) -> Bool { + match predicate { + IsEqual => true + IsNotEqual => false + } +} + +fn canonical_operation_op_add() -> CanonicalOperation { + AlgebraPrimitive { algebra_field: ^ring_field_add } } fn canonical_operation_op_mul() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^ring_field_mul } + AlgebraPrimitive { algebra_field: ^ring_field_mul } } -fn canonical_operation_op_div() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^field_field_reciprocal } +fn canonical_operation_op_negate() -> CanonicalOperation { + AlgebraPrimitive { algebra_field: ^group_field_inverse } } fn canonical_operation_op_and() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^lattice_field_meet } + AlgebraPrimitive { algebra_field: ^lattice_field_meet } } fn canonical_operation_op_or() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^lattice_field_join } + AlgebraPrimitive { algebra_field: ^lattice_field_join } } fn canonical_operation_op_not() -> CanonicalOperation { - AlgebraFieldOperation { algebra_field: ^boolean_algebra_field_complement } + AlgebraPrimitive { algebra_field: ^boolean_algebra_field_complement } } -fn canonical_operation_op_less() -> CanonicalOperation { - OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderLess } +fn canonical_operation_op_sub() -> CanonicalOperation { + AlgebraInverseCompose { + binary_field: ^ring_field_add, + inverse_field: ^group_field_inverse + } } -fn canonical_operation_op_less_or_equal() -> CanonicalOperation { - OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderLessOrEqual } +fn canonical_operation_op_div() -> CanonicalOperation { + AlgebraInverseCompose { + binary_field: ^ring_field_mul, + inverse_field: ^field_field_reciprocal + } } -fn canonical_operation_op_greater() -> CanonicalOperation { - OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderGreater } +fn canonical_operation_op_lt() -> CanonicalOperation { + OrderingComparison { compare_field: ^ordered_ring_field_compare, predicate: IsLess } } -fn canonical_operation_op_greater_or_equal() -> CanonicalOperation { - OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderGreaterOrEqual } +fn canonical_operation_op_le() -> CanonicalOperation { + OrderingComparison { compare_field: ^ordered_ring_field_compare, predicate: IsLessOrEqual } } -fn canonical_operation_op_equal() -> CanonicalOperation { - OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderEqual } +fn canonical_operation_op_gt() -> CanonicalOperation { + OrderingComparison { compare_field: ^ordered_ring_field_compare, predicate: IsGreater } } -fn canonical_operation_op_not_equal() -> CanonicalOperation { - OrderRelationOperation { compare_field: ^ordered_ring_field_compare, relation: OrderNotEqual } +fn canonical_operation_op_ge() -> CanonicalOperation { + OrderingComparison { compare_field: ^ordered_ring_field_compare, predicate: IsGreaterOrEqual } } -fn canonical_order_relation_symbol(relation: CanonicalOrderRelation) -> Symbol { - match relation { - OrderLess => discriminant(v: OrderLess) - OrderLessOrEqual => discriminant(v: OrderLessOrEqual) - OrderGreater => discriminant(v: OrderGreater) - OrderGreaterOrEqual => discriminant(v: OrderGreaterOrEqual) - OrderEqual => discriminant(v: OrderEqual) - OrderNotEqual => discriminant(v: OrderNotEqual) - } +fn canonical_operation_op_eq() -> CanonicalOperation { + EqualityComparison { eq_field: ^equivalence_field_eq, predicate: IsEqual } } -fn canonical_order_relation_from_symbol(id: Symbol) -> Optional { - if id == discriminant(v: OrderLess) { - optional_present(value: OrderLess) - } else { - if id == discriminant(v: OrderLessOrEqual) { - optional_present(value: OrderLessOrEqual) - } else { - if id == discriminant(v: OrderGreater) { - optional_present(value: OrderGreater) - } else { - if id == discriminant(v: OrderGreaterOrEqual) { - optional_present(value: OrderGreaterOrEqual) - } else { - if id == discriminant(v: OrderEqual) { - optional_present(value: OrderEqual) - } else { - if id == discriminant(v: OrderNotEqual) { - optional_present(value: OrderNotEqual) - } else { - optional_absent() - } - } - } - } - } - } -} - -fn canonical_order_relation_equal( - left: CanonicalOrderRelation, - right: CanonicalOrderRelation -) -> Bool { - canonical_order_relation_symbol(relation: left) == canonical_order_relation_symbol(relation: right) +fn canonical_operation_op_ne() -> CanonicalOperation { + EqualityComparison { eq_field: ^equivalence_field_eq, predicate: IsNotEqual } } type TargetOperatorShape @@ -784,7 +772,7 @@ fn target_canonical_operation_wire_malformed_diagnostic(wire: Node) -> Diagnosti } } -fn target_model_canonical_operation_field_symbol_from_wire( +fn target_model_canonical_operation_atom_field_from_wire( wire: Node, field_name: Symbol ) -> Optional { @@ -816,23 +804,67 @@ fn target_model_canonical_operation_field_symbol_from_wire( } } -fn target_model_canonical_operation_relation_from_wire( - wire: Node -) -> Optional { - match target_model_canonical_operation_field_symbol_from_wire( - wire: wire, - field_name: ^target_canonical_operation_field_relation - ) { - Present { value: id } => canonical_order_relation_from_symbol(id: id) - Absent => optional_absent() +fn ordering_predicate_wire_symbol(predicate: OrderingPredicate) -> Symbol { + match predicate { + IsLess => ^ordering_predicate_is_less + IsLessOrEqual => ^ordering_predicate_is_less_or_equal + IsGreater => ^ordering_predicate_is_greater + IsGreaterOrEqual => ^ordering_predicate_is_greater_or_equal + } +} + +fn ordering_predicate_from_wire_symbol(id: Symbol) -> Optional { + if id == ^ordering_predicate_is_less { + optional_present(value: IsLess) + } else { + if id == ^ordering_predicate_is_less_or_equal { + optional_present(value: IsLessOrEqual) + } else { + if id == ^ordering_predicate_is_greater { + optional_present(value: IsGreater) + } else { + if id == ^ordering_predicate_is_greater_or_equal { + optional_present(value: IsGreaterOrEqual) + } else { + optional_absent() + } + } + } + } +} + +fn ordering_predicate_equal(left: OrderingPredicate, right: OrderingPredicate) -> Bool { + ordering_predicate_wire_symbol(predicate: left) == ordering_predicate_wire_symbol(predicate: right) +} + +fn equality_predicate_wire_symbol(predicate: EqualityPredicate) -> Symbol { + match predicate { + IsEqual => ^equality_predicate_is_equal + IsNotEqual => ^equality_predicate_is_not_equal } } +fn equality_predicate_from_wire_symbol(id: Symbol) -> Optional { + if id == ^equality_predicate_is_equal { + optional_present(value: IsEqual) + } else { + if id == ^equality_predicate_is_not_equal { + optional_present(value: IsNotEqual) + } else { + optional_absent() + } + } +} + +fn equality_predicate_equal(left: EqualityPredicate, right: EqualityPredicate) -> Bool { + equality_predicate_wire_symbol(predicate: left) == equality_predicate_wire_symbol(predicate: right) +} + fn target_model_canonical_operation_wire_node(operation: CanonicalOperation) -> Node { match operation { - AlgebraFieldOperation { algebra_field: f } => + AlgebraPrimitive { algebra_field: f } => Node { - kind: TypeNode { connective: Atom { identity: discriminant(v: AlgebraFieldOperation {}) } }, + kind: TypeNode { connective: Atom { identity: discriminant(v: AlgebraPrimitive {}) } }, children: [ target_model_named_edge( name: ^target_canonical_operation_field_algebra_field, @@ -841,19 +873,47 @@ fn target_model_canonical_operation_wire_node(operation: CanonicalOperation) -> ], occurrence_id: SyntheticOccurrence } - OrderRelationOperation { compare_field: cf, relation: r } => + AlgebraInverseCompose { binary_field: b, inverse_field: i } => + Node { + kind: TypeNode { connective: Atom { identity: discriminant(v: AlgebraInverseCompose {}) } }, + children: [ + target_model_named_edge( + name: ^target_canonical_operation_field_binary_field, + target: target_model_type_atom_node(identity: b) + ), + target_model_named_edge( + name: ^target_canonical_operation_field_inverse_field, + target: target_model_type_atom_node(identity: i) + ) + ], + occurrence_id: SyntheticOccurrence + } + OrderingComparison { compare_field: c, predicate: p } => Node { - kind: TypeNode { connective: Atom { identity: discriminant(v: OrderRelationOperation {}) } }, + kind: TypeNode { connective: Atom { identity: discriminant(v: OrderingComparison {}) } }, children: [ target_model_named_edge( name: ^target_canonical_operation_field_compare_field, - target: target_model_type_atom_node(identity: cf) + target: target_model_type_atom_node(identity: c) ), target_model_named_edge( - name: ^target_canonical_operation_field_relation, - target: target_model_type_atom_node( - identity: canonical_order_relation_symbol(relation: r) - ) + name: ^target_canonical_operation_field_predicate, + target: target_model_type_atom_node(identity: ordering_predicate_wire_symbol(predicate: p)) + ) + ], + occurrence_id: SyntheticOccurrence + } + EqualityComparison { eq_field: e, predicate: p } => + Node { + kind: TypeNode { connective: Atom { identity: discriminant(v: EqualityComparison {}) } }, + children: [ + target_model_named_edge( + name: ^target_canonical_operation_field_eq_field, + target: target_model_type_atom_node(identity: e) + ), + target_model_named_edge( + name: ^target_canonical_operation_field_predicate, + target: target_model_type_atom_node(identity: equality_predicate_wire_symbol(predicate: p)) ) ], occurrence_id: SyntheticOccurrence @@ -866,16 +926,36 @@ fn canonical_operation_equal( right: CanonicalOperation ) -> Bool { match left { - AlgebraFieldOperation { algebra_field: lf } => + AlgebraPrimitive { algebra_field: lf } => + match right { + AlgebraPrimitive { algebra_field: rf } => lf == rf + AlgebraInverseCompose { binary_field: _, inverse_field: _ } => false + OrderingComparison { compare_field: _, predicate: _ } => false + EqualityComparison { eq_field: _, predicate: _ } => false + } + AlgebraInverseCompose { binary_field: lb, inverse_field: li } => match right { - AlgebraFieldOperation { algebra_field: rf } => lf == rf - OrderRelationOperation { compare_field: _, relation: _ } => false + AlgebraPrimitive { algebra_field: _ } => false + AlgebraInverseCompose { binary_field: rb, inverse_field: ri } => + lb == rb && li == ri + OrderingComparison { compare_field: _, predicate: _ } => false + EqualityComparison { eq_field: _, predicate: _ } => false } - OrderRelationOperation { compare_field: lcf, relation: lr } => + OrderingComparison { compare_field: lc, predicate: lp } => match right { - AlgebraFieldOperation { algebra_field: _ } => false - OrderRelationOperation { compare_field: rcf, relation: rr } => - lcf == rcf && canonical_order_relation_equal(left: lr, right: rr) + AlgebraPrimitive { algebra_field: _ } => false + AlgebraInverseCompose { binary_field: _, inverse_field: _ } => false + OrderingComparison { compare_field: rc, predicate: rp } => + lc == rc && ordering_predicate_equal(left: lp, right: rp) + EqualityComparison { eq_field: _, predicate: _ } => false + } + EqualityComparison { eq_field: le, predicate: lp } => + match right { + AlgebraPrimitive { algebra_field: _ } => false + AlgebraInverseCompose { binary_field: _, inverse_field: _ } => false + OrderingComparison { compare_field: _, predicate: _ } => false + EqualityComparison { eq_field: re, predicate: rp } => + le == re && equality_predicate_equal(left: lp, right: rp) } } } @@ -883,31 +963,34 @@ fn canonical_operation_equal( fn canonical_operation_from_wire_node(wire: Node) -> Outcome { match wire.kind { TypeNode { connective: Atom { identity: id } } => - if id == discriminant(v: AlgebraFieldOperation {}) { - match target_model_canonical_operation_field_symbol_from_wire( + if id == discriminant(v: AlgebraPrimitive {}) { + match target_model_canonical_operation_atom_field_from_wire( wire: wire, field_name: ^target_canonical_operation_field_algebra_field ) { Present { value: algebra_field } => - outcome_accepted(AlgebraFieldOperation { algebra_field: algebra_field }) + outcome_accepted(AlgebraPrimitive { algebra_field: algebra_field }) Absent => outcome_rejected( target_canonical_operation_wire_malformed_diagnostic(wire: wire) ) } } else { - if id == discriminant(v: OrderRelationOperation {}) { - match target_model_canonical_operation_field_symbol_from_wire( + if id == discriminant(v: AlgebraInverseCompose {}) { + match target_model_canonical_operation_atom_field_from_wire( wire: wire, - field_name: ^target_canonical_operation_field_compare_field + field_name: ^target_canonical_operation_field_binary_field ) { - Present { value: compare_field } => - match target_model_canonical_operation_relation_from_wire(wire: wire) { - Present { value: relation } => + Present { value: binary_field } => + match target_model_canonical_operation_atom_field_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_inverse_field + ) { + Present { value: inverse_field } => outcome_accepted( - OrderRelationOperation { - compare_field: compare_field, - relation: relation + AlgebraInverseCompose { + binary_field: binary_field, + inverse_field: inverse_field } ) Absent => @@ -921,9 +1004,81 @@ fn canonical_operation_from_wire_node(wire: Node) -> Outcome ) } } else { - outcome_rejected( - target_canonical_operation_wire_malformed_diagnostic(wire: wire) - ) + if id == discriminant(v: OrderingComparison {}) { + match target_model_canonical_operation_atom_field_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_compare_field + ) { + Present { value: compare_field } => + match target_model_canonical_operation_atom_field_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_predicate + ) { + Present { value: predicate_id } => + match ordering_predicate_from_wire_symbol(id: predicate_id) { + Present { value: predicate } => + outcome_accepted( + OrderingComparison { + compare_field: compare_field, + predicate: predicate + } + ) + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + } else { + if id == discriminant(v: EqualityComparison {}) { + match target_model_canonical_operation_atom_field_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_eq_field + ) { + Present { value: eq_field } => + match target_model_canonical_operation_atom_field_from_wire( + wire: wire, + field_name: ^target_canonical_operation_field_predicate + ) { + Present { value: predicate_id } => + match equality_predicate_from_wire_symbol(id: predicate_id) { + Present { value: predicate } => + outcome_accepted( + EqualityComparison { + eq_field: eq_field, + predicate: predicate + } + ) + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + Absent => + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + } else { + outcome_rejected( + target_canonical_operation_wire_malformed_diagnostic(wire: wire) + ) + } + } } } _ =>