Skip to content

Consistency check when defining reductions #78

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Charles-Johnson merged 8 commits into from
Dec 10, 2025
Merged

Consistency check when defining reductions #78

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
fb122be
Consistency check when defining reductions
Charles-Johnson Apr 21, 2024
621d292
Merge branch 'master' into extend-relationships-tutorial
Charles-Johnson Oct 10, 2025
cd22db4
Resolve lint and format errors
Charles-Johnson Oct 10, 2025
c91eaf8
Merge remote-tracking branch 'origin/master' into extend-relationship…
Charles-Johnson Dec 10, 2025
efe7240
Merge remote-tracking branch 'origin/master' into extend-relationship…
Charles-Johnson Dec 10, 2025
b90074b
Implement forget concrete concept and fix tests
Charles-Johnson Dec 10, 2025
311ad4c
Fix doc tests
Charles-Johnson Dec 10, 2025
3479807
Fix doc tests
Charles-Johnson Dec 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
104 changes: 68 additions & 36 deletions zia-lang.org/crate/src/generated/css_classes.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@

// DO NOT EDIT THIS FILE - IT'S GENERATED, CHANGES WILL BE LOST!

#[allow(non_snake_case, dead_code)]
Expand Down Expand Up @@ -1592,7 +1591,6 @@ pub struct CssClasses<'a> {
}

pub static C: CssClasses = CssClasses {

/**
width: 100%;
max-width: 569px; @media (min-width: 569px)
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
8 changes: 7 additions & 1 deletion zia-lang.org/crate/src/page/home/tutorials.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#[cfg(test)]
use std::time::{Duration, Instant};

pub const TUTORIALS: (Tutorial<18>, Tutorial<9>, Tutorial<12>) = (
pub const TUTORIALS: (Tutorial<18>, Tutorial<10>, Tutorial<12>) = (
Tutorial {
title: "Factorial",
steps: [
Expand Down Expand Up @@ -154,6 +154,12 @@ pub const TUTORIALS: (Tutorial<18>, Tutorial<9>, Tutorial<12>) = (
#[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",
Expand Down
10 changes: 4 additions & 6 deletions zia/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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");

Expand All @@ -50,7 +51,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("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"), "");
Expand Down Expand Up @@ -87,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");
Expand Down
1 change: 1 addition & 0 deletions zia/src/concepts/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -740,6 +740,7 @@ pub enum ConcreteConceptType {
Implication,
ExistsSuchThat,
Precedes,
Forget,
}

impl<Id: Eq + Hash> From<ConcreteConceptType> for SpecificPart<Id> {
Expand Down
Loading
Loading