From fb122beba072e29b91125271904d7ea10915b5a9 Mon Sep 17 00:00:00 2001 From: Charles Johnson Date: Sun, 21 Apr 2024 11:32:10 +0900 Subject: [PATCH 1/5] Consistency check when defining reductions --- zia-lang.org/crate/src/page/home/tutorials.rs | 8 +++++++- zia/src/context.rs | 16 +++++++++++++--- zia/src/errors.rs | 5 +++++ 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/zia-lang.org/crate/src/page/home/tutorials.rs b/zia-lang.org/crate/src/page/home/tutorials.rs index 1e0e204e..ed6b29eb 100644 --- a/zia-lang.org/crate/src/page/home/tutorials.rs +++ b/zia-lang.org/crate/src/page/home/tutorials.rs @@ -1,4 +1,4 @@ -pub const TUTORIALS: (Tutorial<18>, Tutorial<9>) = ( +pub const TUTORIALS: (Tutorial<18>, Tutorial<10>) = ( Tutorial { title: "Factorial", steps: [ @@ -151,6 +151,12 @@ pub const TUTORIALS: (Tutorial<18>, Tutorial<9>) = ( #[cfg(test)] expected_evaluation: "false" }, + TutorialStep { + command: "let Alice is child of Bob", + explanation: "We won't accidentally define a parent as a child of their child", + #[cfg(test)] + expected_evaluation: "Alice is child of Bob already reduces to false" + }, TutorialStep { command: "let ((_y_ exists_such_that) (_x_ is parent of _y_) and (_y_ is parent of _z_)) => (_x_ is grandparent of _z_)", explanation: "Define grandparent is terms of parent relationships", diff --git a/zia/src/context.rs b/zia/src/context.rs index 7c84216b..0fb1d398 100755 --- a/zia/src/context.rs +++ b/zia/src/context.rs @@ -884,14 +884,23 @@ where fn execute_reduction( &mut self, - syntax: &Syntax, - normal_form: &Syntax, + syntax: &SharedSyntax, + normal_form: &SharedSyntax, ) -> ZiaResult<()> { if normal_form.contains(syntax) { Err(ZiaError::ExpandingReduction) } else if syntax == normal_form { self.try_removing_reduction(syntax) } else { + let context_search = self.context_search(); + if let Some((existing_reduction, _)) = context_search + .reduce(syntax) + .or_else(|| context_search + .find_examples_of_inferred_reduction(syntax) + ) { + Err(ZiaError::ExistingReduction{syntax_to_reduce: syntax.to_string(), existing_reduction: existing_reduction.to_string()}) + } else { + drop(context_search); let maybe_inner_delta = self.delta.get_mut(); let Some(delta) = maybe_inner_delta else { return Err(ZiaError::MultiplePointersToDelta); @@ -904,7 +913,8 @@ where }; let syntax_concept = updater.concept_from_ast(syntax)?; let normal_form_concept = updater.concept_from_ast(normal_form)?; - updater.update_reduction(syntax_concept, normal_form_concept) + updater.update_reduction(syntax_concept, normal_form_concept) + } } } diff --git a/zia/src/errors.rs b/zia/src/errors.rs index cfdd59e6..b76bfd0e 100755 --- a/zia/src/errors.rs +++ b/zia/src/errors.rs @@ -99,4 +99,9 @@ pub enum ZiaError { CanOnlyQuantifyOverVariables, #[error("Multiple smart pointers to context delta")] MultiplePointersToDelta, + #[error("{syntax_to_reduce} already reduces to {existing_reduction}")] + ExistingReduction { + syntax_to_reduce: String, + existing_reduction: String, + }, } From cd22db48263d02640180489c88eedf12bb7b2466 Mon Sep 17 00:00:00 2001 From: Charle Johnson Date: Fri, 10 Oct 2025 18:33:20 +0000 Subject: [PATCH 2/5] Resolve lint and format errors --- .../crate/src/generated/css_classes.rs | 104 ++++++++++++------ zia-lang.org/crate/src/page/home/tutorials.rs | 1 - zia/src/context.rs | 20 ++-- 3 files changed, 79 insertions(+), 46 deletions(-) diff --git a/zia-lang.org/crate/src/generated/css_classes.rs b/zia-lang.org/crate/src/generated/css_classes.rs index 874154f9..5db2f2ad 100644 --- a/zia-lang.org/crate/src/generated/css_classes.rs +++ b/zia-lang.org/crate/src/generated/css_classes.rs @@ -1,4 +1,3 @@ - // DO NOT EDIT THIS FILE - IT'S GENERATED, CHANGES WILL BE LOST! #[allow(non_snake_case, dead_code)] @@ -1592,7 +1591,6 @@ pub struct CssClasses<'a> { } pub static C: CssClasses = CssClasses { - /** width: 100%; max-width: 569px; @media (min-width: 569px) @@ -3459,7 +3457,8 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; background-color: rgba(255, 0, 0, var(--tw-bg-opacity)); */ - group_hover__bg_unmatched_parenthesis: "group-hover:bg-unmatched_parenthesis", + group_hover__bg_unmatched_parenthesis: + "group-hover:bg-unmatched_parenthesis", /** --tw-bg-opacity: 1; @@ -3501,7 +3500,8 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; background-color: rgba(255, 0, 0, var(--tw-bg-opacity)); */ - focus_within__bg_unmatched_parenthesis: "focus-within:bg-unmatched_parenthesis", + focus_within__bg_unmatched_parenthesis: + "focus-within:bg-unmatched_parenthesis", /** --tw-bg-opacity: 1; @@ -4069,7 +4069,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; color: rgba(255, 0, 0, var(--tw-text-opacity)); */ - group_hover__text_unmatched_parenthesis: "group-hover:text-unmatched_parenthesis", + group_hover__text_unmatched_parenthesis: + "group-hover:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @@ -4111,7 +4112,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; color: rgba(255, 0, 0, var(--tw-text-opacity)); */ - focus_within__text_unmatched_parenthesis: "focus-within:text-unmatched_parenthesis", + focus_within__text_unmatched_parenthesis: + "focus-within:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @@ -6370,7 +6372,8 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; @media (min-width: 569px) background-color: rgba(255, 0, 0, var(--tw-bg-opacity)); @media (min-width: 569px) */ - sm__group_hover__bg_unmatched_parenthesis: "sm:group-hover:bg-unmatched_parenthesis", + sm__group_hover__bg_unmatched_parenthesis: + "sm:group-hover:bg-unmatched_parenthesis", /** --tw-bg-opacity: 1; @media (min-width: 569px) @@ -6388,19 +6391,22 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; @media (min-width: 569px) background-color: rgba(255, 191, 0, var(--tw-bg-opacity)); @media (min-width: 569px) */ - sm__focus_within__bg_variable_concept: "sm:focus-within:bg-variable_concept", + sm__focus_within__bg_variable_concept: + "sm:focus-within:bg-variable_concept", /** --tw-bg-opacity: 1; @media (min-width: 569px) background-color: rgba(191, 0, 255, var(--tw-bg-opacity)); @media (min-width: 569px) */ - sm__focus_within__bg_abstract_concept: "sm:focus-within:bg-abstract_concept", + sm__focus_within__bg_abstract_concept: + "sm:focus-within:bg-abstract_concept", /** --tw-bg-opacity: 1; @media (min-width: 569px) background-color: rgba(64, 0, 255, var(--tw-bg-opacity)); @media (min-width: 569px) */ - sm__focus_within__bg_concrete_concept: "sm:focus-within:bg-concrete_concept", + sm__focus_within__bg_concrete_concept: + "sm:focus-within:bg-concrete_concept", /** --tw-bg-opacity: 1; @media (min-width: 569px) @@ -6412,7 +6418,8 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; @media (min-width: 569px) background-color: rgba(255, 0, 0, var(--tw-bg-opacity)); @media (min-width: 569px) */ - sm__focus_within__bg_unmatched_parenthesis: "sm:focus-within:bg-unmatched_parenthesis", + sm__focus_within__bg_unmatched_parenthesis: + "sm:focus-within:bg-unmatched_parenthesis", /** --tw-bg-opacity: 1; @media (min-width: 569px) @@ -6956,19 +6963,22 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(255, 191, 0, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__group_hover__text_variable_concept: "sm:group-hover:text-variable_concept", + sm__group_hover__text_variable_concept: + "sm:group-hover:text-variable_concept", /** --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(191, 0, 255, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__group_hover__text_abstract_concept: "sm:group-hover:text-abstract_concept", + sm__group_hover__text_abstract_concept: + "sm:group-hover:text-abstract_concept", /** --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(64, 0, 255, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__group_hover__text_concrete_concept: "sm:group-hover:text-concrete_concept", + sm__group_hover__text_concrete_concept: + "sm:group-hover:text-concrete_concept", /** --tw-text-opacity: 1; @media (min-width: 569px) @@ -6980,7 +6990,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__group_hover__text_unmatched_parenthesis: "sm:group-hover:text-unmatched_parenthesis", + sm__group_hover__text_unmatched_parenthesis: + "sm:group-hover:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @media (min-width: 569px) @@ -6998,19 +7009,22 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(255, 191, 0, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__focus_within__text_variable_concept: "sm:focus-within:text-variable_concept", + sm__focus_within__text_variable_concept: + "sm:focus-within:text-variable_concept", /** --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(191, 0, 255, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__focus_within__text_abstract_concept: "sm:focus-within:text-abstract_concept", + sm__focus_within__text_abstract_concept: + "sm:focus-within:text-abstract_concept", /** --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(64, 0, 255, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__focus_within__text_concrete_concept: "sm:focus-within:text-concrete_concept", + sm__focus_within__text_concrete_concept: + "sm:focus-within:text-concrete_concept", /** --tw-text-opacity: 1; @media (min-width: 569px) @@ -7022,7 +7036,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__focus_within__text_unmatched_parenthesis: "sm:focus-within:text-unmatched_parenthesis", + sm__focus_within__text_unmatched_parenthesis: + "sm:focus-within:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @media (min-width: 569px) @@ -7064,7 +7079,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__hover__text_unmatched_parenthesis: "sm:hover:text-unmatched_parenthesis", + sm__hover__text_unmatched_parenthesis: + "sm:hover:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @media (min-width: 569px) @@ -7106,7 +7122,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 569px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 569px) */ - sm__focus__text_unmatched_parenthesis: "sm:focus:text-unmatched_parenthesis", + sm__focus__text_unmatched_parenthesis: + "sm:focus:text-unmatched_parenthesis", /** text-decoration: underline; @media (min-width: 569px) @@ -9261,7 +9278,8 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; @media (min-width: 1025px) background-color: rgba(255, 0, 0, var(--tw-bg-opacity)); @media (min-width: 1025px) */ - lg__group_hover__bg_unmatched_parenthesis: "lg:group-hover:bg-unmatched_parenthesis", + lg__group_hover__bg_unmatched_parenthesis: + "lg:group-hover:bg-unmatched_parenthesis", /** --tw-bg-opacity: 1; @media (min-width: 1025px) @@ -9279,19 +9297,22 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; @media (min-width: 1025px) background-color: rgba(255, 191, 0, var(--tw-bg-opacity)); @media (min-width: 1025px) */ - lg__focus_within__bg_variable_concept: "lg:focus-within:bg-variable_concept", + lg__focus_within__bg_variable_concept: + "lg:focus-within:bg-variable_concept", /** --tw-bg-opacity: 1; @media (min-width: 1025px) background-color: rgba(191, 0, 255, var(--tw-bg-opacity)); @media (min-width: 1025px) */ - lg__focus_within__bg_abstract_concept: "lg:focus-within:bg-abstract_concept", + lg__focus_within__bg_abstract_concept: + "lg:focus-within:bg-abstract_concept", /** --tw-bg-opacity: 1; @media (min-width: 1025px) background-color: rgba(64, 0, 255, var(--tw-bg-opacity)); @media (min-width: 1025px) */ - lg__focus_within__bg_concrete_concept: "lg:focus-within:bg-concrete_concept", + lg__focus_within__bg_concrete_concept: + "lg:focus-within:bg-concrete_concept", /** --tw-bg-opacity: 1; @media (min-width: 1025px) @@ -9303,7 +9324,8 @@ pub static C: CssClasses = CssClasses { --tw-bg-opacity: 1; @media (min-width: 1025px) background-color: rgba(255, 0, 0, var(--tw-bg-opacity)); @media (min-width: 1025px) */ - lg__focus_within__bg_unmatched_parenthesis: "lg:focus-within:bg-unmatched_parenthesis", + lg__focus_within__bg_unmatched_parenthesis: + "lg:focus-within:bg-unmatched_parenthesis", /** --tw-bg-opacity: 1; @media (min-width: 1025px) @@ -9847,19 +9869,22 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(255, 191, 0, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__group_hover__text_variable_concept: "lg:group-hover:text-variable_concept", + lg__group_hover__text_variable_concept: + "lg:group-hover:text-variable_concept", /** --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(191, 0, 255, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__group_hover__text_abstract_concept: "lg:group-hover:text-abstract_concept", + lg__group_hover__text_abstract_concept: + "lg:group-hover:text-abstract_concept", /** --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(64, 0, 255, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__group_hover__text_concrete_concept: "lg:group-hover:text-concrete_concept", + lg__group_hover__text_concrete_concept: + "lg:group-hover:text-concrete_concept", /** --tw-text-opacity: 1; @media (min-width: 1025px) @@ -9871,7 +9896,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__group_hover__text_unmatched_parenthesis: "lg:group-hover:text-unmatched_parenthesis", + lg__group_hover__text_unmatched_parenthesis: + "lg:group-hover:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @media (min-width: 1025px) @@ -9889,19 +9915,22 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(255, 191, 0, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__focus_within__text_variable_concept: "lg:focus-within:text-variable_concept", + lg__focus_within__text_variable_concept: + "lg:focus-within:text-variable_concept", /** --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(191, 0, 255, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__focus_within__text_abstract_concept: "lg:focus-within:text-abstract_concept", + lg__focus_within__text_abstract_concept: + "lg:focus-within:text-abstract_concept", /** --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(64, 0, 255, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__focus_within__text_concrete_concept: "lg:focus-within:text-concrete_concept", + lg__focus_within__text_concrete_concept: + "lg:focus-within:text-concrete_concept", /** --tw-text-opacity: 1; @media (min-width: 1025px) @@ -9913,7 +9942,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__focus_within__text_unmatched_parenthesis: "lg:focus-within:text-unmatched_parenthesis", + lg__focus_within__text_unmatched_parenthesis: + "lg:focus-within:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @media (min-width: 1025px) @@ -9955,7 +9985,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__hover__text_unmatched_parenthesis: "lg:hover:text-unmatched_parenthesis", + lg__hover__text_unmatched_parenthesis: + "lg:hover:text-unmatched_parenthesis", /** --tw-text-opacity: 1; @media (min-width: 1025px) @@ -9997,7 +10028,8 @@ pub static C: CssClasses = CssClasses { --tw-text-opacity: 1; @media (min-width: 1025px) color: rgba(255, 0, 0, var(--tw-text-opacity)); @media (min-width: 1025px) */ - lg__focus__text_unmatched_parenthesis: "lg:focus:text-unmatched_parenthesis", + lg__focus__text_unmatched_parenthesis: + "lg:focus:text-unmatched_parenthesis", /** text-decoration: underline; @media (min-width: 1025px) diff --git a/zia-lang.org/crate/src/page/home/tutorials.rs b/zia-lang.org/crate/src/page/home/tutorials.rs index 5270468e..d185acd4 100644 --- a/zia-lang.org/crate/src/page/home/tutorials.rs +++ b/zia-lang.org/crate/src/page/home/tutorials.rs @@ -1,4 +1,3 @@ - #[cfg(test)] use std::time::{Duration, Instant}; diff --git a/zia/src/context.rs b/zia/src/context.rs index f913d6d6..9b7d511b 100755 --- a/zia/src/context.rs +++ b/zia/src/context.rs @@ -1160,15 +1160,17 @@ where self.try_removing_reduction(syntax) } else { let context_search = self.context_search(); - if let Some((existing_reduction, _)) = context_search - .reduce(syntax) - .or_else(|| context_search - .find_examples_of_inferred_reduction(syntax) - ) { - return Err(ZiaError::ExistingReduction{syntax_to_reduce: syntax.to_string(), existing_reduction: existing_reduction.to_string()}); - } else { - drop(context_search); - } + if let Some((existing_reduction, _)) = + context_search.reduce(syntax).or_else(|| { + context_search.find_examples_of_inferred_reduction(syntax) + }) + { + return Err(ZiaError::ExistingReduction { + syntax_to_reduce: syntax.to_string(), + existing_reduction: existing_reduction.to_string(), + }); + } + drop(context_search); let maybe_inner_delta = self.delta.get_mut(); let Some(delta) = maybe_inner_delta else { return Err(ZiaError::MultiplePointersToDelta); From b90074bb45a90a834d99afed5c2f7dfe9cf9ffdc Mon Sep 17 00:00:00 2001 From: Charle Johnson Date: Wed, 10 Dec 2025 21:50:26 +0000 Subject: [PATCH 3/5] Implement forget concrete concept and fix tests --- zia/README.md | 5 ++-- zia/src/concepts/mod.rs | 1 + zia/src/context.rs | 5 ++++ zia/src/context_search.rs | 54 +-------------------------------------- zia/src/lib.rs | 5 ++-- zia/tests/reductions.rs | 7 +++-- 6 files changed, 18 insertions(+), 59 deletions(-) diff --git a/zia/README.md b/zia/README.md index c5cda61d..d33fbd42 100755 --- a/zia/README.md +++ b/zia/README.md @@ -21,8 +21,8 @@ binary tree of height 2 with leaves `"ll"`, `"lr"`, `"rl"`, `"rr"` going from le The leaves of the tree can be any unicode string without spaces or parentheses. These symbols may be recognised by the intepreter as concepts or if not used to label new concepts. -So far there are 10 built-in concepts. A new `Context` labels these with the symbols, `label_of`, -`->`, `:=`, `let`, `true`, `false`, `assoc`, `right`, `left`, `precedes`, `>`, `=>` and +So far there are 14 built-in concepts. A new `Context` labels these with the symbols, `label_of`, +`->`, `:=`, `let`, `true`, `false`, `assoc`, `right`, `left`, `precedes`, `>`, `=>`, `forget` and `exists_such_that` but the concepts can be renamed (via the `:=` concept, as shown below) to different symbols for different languages or disciplines. @@ -49,6 +49,7 @@ assert_eq!(context.execute("a b"), "a b"); // Try to specify a rule that already exists assert_eq!(context.execute("let a b -> a b"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); +assert_eq!(context.execute("forget a b"), ""); assert_eq!(context.execute("let a b -> c"), ""); assert_eq!(context.execute("let a b -> c"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); diff --git a/zia/src/concepts/mod.rs b/zia/src/concepts/mod.rs index ce6058cf..63576802 100755 --- a/zia/src/concepts/mod.rs +++ b/zia/src/concepts/mod.rs @@ -740,6 +740,7 @@ pub enum ConcreteConceptType { Implication, ExistsSuchThat, Precedes, + Forget, } impl From for SpecificPart { diff --git a/zia/src/context.rs b/zia/src/context.rs index 9b7d511b..0f018b62 100755 --- a/zia/src/context.rs +++ b/zia/src/context.rs @@ -800,6 +800,7 @@ where ("=>", ConcreteConceptType::Implication), ("exists_such_that", ConcreteConceptType::ExistsSuchThat), ("precedes", ConcreteConceptType::Precedes), + ("forget", ConcreteConceptType::Forget), ]; let maybe_inner_delta = self.delta.get_mut(); let Some(delta) = maybe_inner_delta else { @@ -956,6 +957,10 @@ where maybe_ast.map(|ast| self.execute_reduction(right, &ast)) }) .map(|r| r.map(|()| String::new())), + ConcreteConceptType::Forget => right.get_concept().map(|c| { + self.updater()?.delete_reduction(c, right.to_string())?; + Ok(String::new()) + }), ConcreteConceptType::Label => Some(Ok("'".to_string() + &right .get_concept() diff --git a/zia/src/context_search.rs b/zia/src/context_search.rs index b6ad15b5..66613269 100644 --- a/zia/src/context_search.rs +++ b/zia/src/context_search.rs @@ -171,41 +171,6 @@ where }) } - // If (operator right) cannot by trying be reduced by other means, then it should reduce to default_concept - fn reduce_otherwise_default( - &self, - ast: &SharedSyntax, - left: &SharedSyntax, - right: &SharedSyntax, - operator_id: &S::ConceptId, - default_concept_id: &S::ConceptId, - ) -> ReductionResult { - let mut reduced_pair: ReductionResult = None; - let mut operator_composition_check = || { - let cache = SR::share(ReductionCache::::default()); - let mut context_search = self.spawn(&cache, self.delta.clone()); - context_search.syntax_evaluating.insert(ast.key()); - reduced_pair = context_search.reduce_pair(left, right); - let operator_concept = - self.snap_shot.read_concept(self.delta.as_ref(), *operator_id); - let find = |c| { - operator_concept.find_as_hand_in_composition_with(c, Hand::Left) - }; - reduced_pair.is_none() - && right.get_concept().and_then(find).is_none() - }; - if self.syntax_evaluating.contains(&ast.key()) - || operator_composition_check() - { - Some(( - self.to_ast(default_concept_id), - ReductionReason::::default(*operator_id), - )) - } else { - reduced_pair - } - } - /// Reduces the syntax by using the reduction rules of associated concepts. pub fn reduce( &self, @@ -223,24 +188,7 @@ where .and_then(|c| self.reduce_concept(&c)) .or_else(|| { let (ref left, ref right) = ast.get_expansion()?; - left.get_concept() - .and_then(|lc| match self.concrete_type(&lc) { - Some(ConcreteConceptType::Associativity) => { - let default_concept_id = self - .concrete_concept_id( - ConcreteConceptType::Right, - )?; - self.reduce_otherwise_default( - ast, - left, - right, - &lc, - &default_concept_id, - ) - }, - _ => None, - }) - .or_else(|| self.reduce_pair(left, right)) + self.reduce_pair(left, right) }); self.caches.insert_reduction(ast, &reduction_result); reduction_result diff --git a/zia/src/lib.rs b/zia/src/lib.rs index 58242614..6bbc1232 100755 --- a/zia/src/lib.rs +++ b/zia/src/lib.rs @@ -33,8 +33,8 @@ //! The leaves of the tree can be any unicode string without spaces or parentheses. These symbols may //! be recognised by the intepreter as concepts or if not used to label new concepts. //! -//! So far there are 10 built-in concepts. A new `Context` labels these with the symbols, `label_of`, -//! `->`, `:=`, `let`, `true`, `false`, `assoc`, `right`, `left`, `precedes`, `>`, `=>` and +//! So far there are 14 built-in concepts. A new `Context` labels these with the symbols, `label_of`, +//! `->`, `:=`, `let`, `true`, `false`, `assoc`, `right`, `left`, `precedes`, `>`, `=>`, `forget` and //! `exists_such_that` but the concepts can be renamed (via the `:=` concept, as shown below) to //! different symbols for different languages or disciplines. //! @@ -61,6 +61,7 @@ //! //! // Try to specify a rule that already exists //! assert_eq!(context.execute("let a b -> a b"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); +//! assert_eq!(context.execute("forget a b"), ""); //! assert_eq!(context.execute("let a b -> c"), ""); //! assert_eq!(context.execute("let a b -> c"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); //! diff --git a/zia/tests/reductions.rs b/zia/tests/reductions.rs index 8a8c8148..8ed3e017 100644 --- a/zia/tests/reductions.rs +++ b/zia/tests/reductions.rs @@ -81,6 +81,7 @@ fn broken_middle_chain() { fn change_reduction_rule() { let mut cont = NEW_CONTEXT.clone(); assert_eq!(cont.execute("let a b -> c"), ""); + assert_eq!(cont.execute("forget a b"), ""); assert_eq!(cont.execute("let a b -> d"), ""); assert_eq!(cont.execute("a b"), "d"); } @@ -90,6 +91,7 @@ fn leapfrog_reduction_rule() { let mut cont = NEW_CONTEXT.clone(); assert_eq!(cont.execute("let a b -> c d"), ""); assert_eq!(cont.execute("let c d -> e"), ""); + assert_eq!(cont.execute("forget a b"), ""); assert_eq!(cont.execute("let a b -> e"), ""); } // It is redundant to specify a reduction rule that is already true @@ -99,8 +101,9 @@ fn redundancy() { assert_eq!(cont.execute("let a b -> c"), ""); assert_eq!( cont.execute("let a b -> c"), - ZiaError::RedundantReduction { - syntax: "a b".into() + ZiaError::ExistingReduction { + syntax_to_reduce: "a b".into(), + existing_reduction: "c".into() } .to_string() ); From 311ad4c0eb3add8c8b217a997fe45f0746a7e2a5 Mon Sep 17 00:00:00 2001 From: Charle Johnson Date: Wed, 10 Dec 2025 22:02:04 +0000 Subject: [PATCH 4/5] Fix doc tests --- zia/src/lib.rs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/zia/src/lib.rs b/zia/src/lib.rs index 6bbc1232..efbddf6b 100755 --- a/zia/src/lib.rs +++ b/zia/src/lib.rs @@ -52,6 +52,7 @@ //! assert_eq!(context.execute("a b"), "c"); //! //! // Change the rule so that concept "a b" instead reduces to concept "d" +//! assert_eq!(context.execute("forget a b"), ""); //! assert_eq!(context.execute("let a b -> d"), ""); //! assert_eq!(context.execute("a b"), "d"); //! @@ -61,9 +62,8 @@ //! //! // Try to specify a rule that already exists //! assert_eq!(context.execute("let a b -> a b"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); -//! assert_eq!(context.execute("forget a b"), ""); //! assert_eq!(context.execute("let a b -> c"), ""); -//! assert_eq!(context.execute("let a b -> c"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); +//! assert_eq!(context.execute("let a b -> c"), ZiaError::ExistingReduction{syntax_to_reduce: "a b".to_string(), existing_reduction: "c".to_string()}.to_string()); //! //! // Relabel "label_of" to "표시" //! assert_eq!(context.execute("let 표시 := label_of"), ""); @@ -100,9 +100,6 @@ //! assert_eq!(context.execute("let h i j"), ""); //! assert_eq!(context.execute("h i j"), "true"); //! -//! // Determine associativity of symbol -//! assert_eq!(context.execute("assoc a"), "right"); -//! //! // Define patterns //! assert_eq!(context.execute("let _x_ or true -> true"), ""); //! assert_eq!(context.execute("false or true"), "true"); From 347980723ed5614d47879f08918889b702ffff89 Mon Sep 17 00:00:00 2001 From: Charle Johnson Date: Wed, 10 Dec 2025 22:03:06 +0000 Subject: [PATCH 5/5] Fix doc tests --- zia/README.md | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/zia/README.md b/zia/README.md index d33fbd42..f78c7527 100755 --- a/zia/README.md +++ b/zia/README.md @@ -40,6 +40,7 @@ assert_eq!(context.execute("let a b -> c"), ""); assert_eq!(context.execute("a b"), "c"); // Change the rule so that concept "a b" instead reduces to concept "d" +assert_eq!(context.execute("forget a b"), ""); assert_eq!(context.execute("let a b -> d"), ""); assert_eq!(context.execute("a b"), "d"); @@ -49,9 +50,8 @@ assert_eq!(context.execute("a b"), "a b"); // Try to specify a rule that already exists assert_eq!(context.execute("let a b -> a b"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); -assert_eq!(context.execute("forget a b"), ""); assert_eq!(context.execute("let a b -> c"), ""); -assert_eq!(context.execute("let a b -> c"), ZiaError::RedundantReduction{syntax: "a b".to_string()}.to_string()); +assert_eq!(context.execute("let a b -> c"), ZiaError::ExistingReduction{syntax_to_reduce: "a b".to_string(), existing_reduction: "c".to_string()}.to_string()); // Relabel "label_of" to "표시" assert_eq!(context.execute("let 표시 := label_of"), ""); @@ -88,9 +88,6 @@ assert_eq!(context.execute("g"), "true"); assert_eq!(context.execute("let h i j"), ""); assert_eq!(context.execute("h i j"), "true"); -// Determine associativity of symbol -assert_eq!(context.execute("assoc a"), "right"); - // Define patterns assert_eq!(context.execute("let _x_ or true -> true"), ""); assert_eq!(context.execute("false or true"), "true");