diff --git a/zia-lang.org/crate/src/page/home/tutorials.rs b/zia-lang.org/crate/src/page/home/tutorials.rs index 68375c1..9c35417 100644 --- a/zia-lang.org/crate/src/page/home/tutorials.rs +++ b/zia-lang.org/crate/src/page/home/tutorials.rs @@ -1,7 +1,7 @@ #[cfg(test)] use std::time::{Duration, Instant}; -pub const TUTORIALS: (Tutorial<18>, Tutorial<10>, Tutorial<18>) = ( +pub const TUTORIALS: (Tutorial<18>, Tutorial<12>, Tutorial<18>) = ( Tutorial { title: "Factorial", steps: [ @@ -177,7 +177,25 @@ pub const TUTORIALS: (Tutorial<18>, Tutorial<10>, Tutorial<18>) = ( explanation: "Let's check", #[cfg(test)] expected_evaluation: "true" - } + }, + TutorialStep { + command: "let ((_y_ exists_such_that) (_y_ is parent of _x_) and (_y_ is parent of _z_)) => (_x_ is sibling of _z_)", + explanation: "Define sibling is terms of parent relationships", + #[cfg(test)] + expected_evaluation: "" + }, + TutorialStep { + command: "let Alice is parent of Eve", + explanation: "This should mean that Eve is sibling of Bob", + #[cfg(test)] + expected_evaluation: "" + }, + //TutorialStep { + // command: "Eve is sibling of Bob", + // explanation: "Let's check", + // #[cfg(test)] + // expected_evaluation: "true" + //} ] }, Tutorial { diff --git a/zia/src/context_search.rs b/zia/src/context_search.rs index 301ffd0..7a41a71 100644 --- a/zia/src/context_search.rs +++ b/zia/src/context_search.rs @@ -29,9 +29,15 @@ use crate::{ substitute::substitute, variable_mask_list::{VariableMask, VariableMaskList}, }; +use dashmap::DashSet; use log::debug; use maplit::{hashmap, hashset}; -use std::{collections::HashSet, fmt::Debug, iter, marker::PhantomData}; +use std::{ + collections::HashSet, + fmt::Debug, + iter::{self, empty}, + marker::PhantomData, +}; pub struct ContextSearch<'s, 'v, S, CCI: ConceptId, SR: SharedReference> where @@ -213,9 +219,9 @@ where let cache = SR::share(ReductionCache::::default()); match (left_result, right_result) { (None, None) => { - let ast = self.contract_pair(left, right); - let generalisation_candidates = self.find_generalisations(&ast); - let ast = ast.share(); + let ast = SR::share(self.contract_pair(left, right)); + let generalisation_candidates = + self.find_generalisations(ast.as_ref())?; generalisation_candidates .into_iter() .filter_map(move |gc| { @@ -340,42 +346,16 @@ where .bind_pair(lefthand.clone(), righthand.clone()) } - fn find_generalisations( - &self, + fn find_generalisations<'a>( + &'a self, ast: &GenericSyntaxTree, - ) -> HashSet { - let mut generalisations = HashSet::::new(); - if let Some((l, r)) = ast.get_expansion() { - if let Some(c) = l.get_concept() { - generalisations.extend( - self.snap_shot - .read_concept(self.delta.as_ref(), c) - .iter_composition_ids(Hand::Left), - ); - } - if let Some(c) = r.get_concept() { - generalisations.extend( - self.snap_shot - .read_concept(self.delta.as_ref(), c) - .iter_composition_ids(Hand::Right), - ); - } - self.find_generalisations(&l).iter().for_each(|g| { - generalisations.extend( - self.snap_shot - .read_concept(self.delta.as_ref(), *g) - .iter_composition_ids(Hand::Left), - ); - }); - self.find_generalisations(&r).iter().for_each(|g| { - generalisations.extend( - self.snap_shot - .read_concept(self.delta.as_ref(), *g) - .iter_composition_ids(Hand::Right), - ); - }); - } - generalisations + ) -> Option + 'a> { + GeneralisationFinder::<'a, S, CCI, SR>::new( + ast, + self.snap_shot, + self.delta.clone(), + SR::share(DashSet::default()), + ) } /// Reduces the syntax as much as possible (returns the normal form syntax). @@ -564,6 +544,11 @@ where }) }) }); + for item in spawned_context_search.caches.reductions.head.as_ref() { + if let Some(c) = item.key().concept { + self.caches.insert_reduction(&self.to_ast(&c), item.value()); + } + } result } @@ -712,7 +697,7 @@ where }, (true, false) => Box::new( self.find_examples_of_half_generalisation( - left.clone(), + &left, right.clone(), equivalence_set, Hand::Right, @@ -721,7 +706,7 @@ where ), (false, true) => Box::new( self.find_examples_of_half_generalisation( - right.clone(), + &right, left.clone(), equivalence_set, Hand::Left, @@ -735,54 +720,89 @@ where fn find_examples_of_half_generalisation<'a>( &'a self, - generalised_part: SharedSyntax, + generalised_part: &SharedSyntax, non_generalised_part: SharedSyntax, mut equivalence_set_of_composition: impl Iterator + 'a, non_generalised_hand: Hand, ) -> Option> { debug!("find_examples_of_half_generalisation({}, {}, {non_generalised_hand:?})", generalised_part.as_ref(), non_generalised_part.as_ref()); - let non_generalised_part_clone = non_generalised_part.clone(); - let generalised_part_clone = generalised_part; // TODO try to test if this needs to be a flat_map call equivalence_set_of_composition.find_map(move |equivalent_concept_id| { - let equivalent_concept = self - .snap_shot - .read_concept(self.delta.as_ref(), equivalent_concept_id); - let (left, right) = equivalent_concept.get_composition()?; - let (equivalent_non_generalised_hand, equivalent_generalised_hand) = match non_generalised_hand { + self.find_example_of_half_generalisation( + generalised_part, + &non_generalised_part, + equivalent_concept_id, + non_generalised_hand, + |example_hand| { + // TODO handle case when a concept implicitly reduces to `non_generalised_hand` + let equivalence_set = iter::once(example_hand); + let non_generalised_hand_concept = self + .snap_shot + .read_concept(self.delta.as_ref(), example_hand); + self.find_example( + generalised_part, + equivalence_set.chain( + non_generalised_hand_concept + .find_what_reduces_to_it(), + ), + ) + }, + ) + }) + } + + fn find_example_of_half_generalisation( + &self, + generalised_part_clone: &SharedSyntax, + non_generalised_part: &SharedSyntax, + equivalent_concept_id: S::ConceptId, + non_generalised_hand: Hand, + or_else: impl FnOnce(S::ConceptId) -> Option>, + ) -> Option> { + // TODO cache this calculation + let equivalent_concept = self + .snap_shot + .read_concept(self.delta.as_ref(), equivalent_concept_id); + let (left, right) = equivalent_concept.get_composition()?; + let (equivalent_non_generalised_hand, equivalent_generalised_hand) = + match non_generalised_hand { Hand::Left => (left, right), - Hand::Right => (right, left) + Hand::Right => (right, left), }; - if Some(equivalent_non_generalised_hand) != non_generalised_part_clone.get_concept() { - if self.snap_shot.read_concept(self.delta.as_ref(), equivalent_non_generalised_hand).free_variable() { - return self.find_example(&generalised_part_clone, iter::once(equivalent_generalised_hand)).and_then(|subs| { + if Some(equivalent_non_generalised_hand) + != non_generalised_part.get_concept() + { + if self + .snap_shot + .read_concept( + self.delta.as_ref(), + equivalent_non_generalised_hand, + ) + .free_variable() + { + return self.find_example(generalised_part_clone, iter::once(equivalent_generalised_hand)).and_then(|subs| { // Could have a more efficient method for this - subs.consistent_merge(ExampleSubstitutions{example: hashmap!{equivalent_non_generalised_hand => non_generalised_part_clone.clone()}, ..Default::default()}) - }) - } - return None; + subs.consistent_merge(ExampleSubstitutions{example: hashmap!{equivalent_non_generalised_hand => non_generalised_part.clone()}, ..Default::default()}) + }); } - self.find_example(&generalised_part_clone, iter::once(equivalent_generalised_hand)).or_else(|| { - let non_generalised_id = non_generalised_part.get_concept()?; - let example_hand = match non_generalised_hand { - Hand::Left => (left == non_generalised_id).then_some(right)?, - Hand::Right => (right == non_generalised_id).then_some(left)?, - }; - let example_hand_syntax = self.to_ast(&example_hand); - GenericSyntaxTree::::check_example( - &example_hand_syntax, - &generalised_part_clone, - ) - .or_else(|| { - // TODO handle case when a concept implicitly reduces to `non_generalised_hand` - let equivalence_set = iter::once(example_hand); - let non_generalised_hand_concept = self - .snap_shot - .read_concept(self.delta.as_ref(), example_hand); - self.find_example(&generalised_part_clone, equivalence_set.chain(non_generalised_hand_concept - .find_what_reduces_to_it())) - }) - }) + return None; + } + self.find_example( + generalised_part_clone, + iter::once(equivalent_generalised_hand), + ) + .or_else(|| { + let non_generalised_id = non_generalised_part.get_concept()?; + let example_hand = match non_generalised_hand { + Hand::Left => (left == non_generalised_id).then_some(right)?, + Hand::Right => (right == non_generalised_id).then_some(left)?, + }; + let example_hand_syntax = self.to_ast(&example_hand); + GenericSyntaxTree::::check_example( + &example_hand_syntax, + generalised_part_clone, + ) + .or_else(|| or_else(example_hand)) }) } @@ -1269,10 +1289,146 @@ where } } -// struct GeneralisationFinder<'a, CI, SR> { -// ast: &'a GenericSyntaxTree, -// snap_shot: & -//} +struct GeneralisationFinder< + 'a, + S: SnapShotReader, + CI: ConceptId + 'static, + SR: SharedReference, +> { + snap_shot: &'a S, + generalisations: SR::Share>, + delta: SR::Share>, + concepts_used: bool, + composition_id_iter: Box>, + left_syntax: SR::Share>, + right_syntax: SR::Share>, + left_finder: Option>, + right_finder: Option>, +} + +impl< + 'a, + S: SnapShotReader, + CI: ConceptId + 'static, + SR: SharedReference, + > GeneralisationFinder<'a, S, CI, SR> +{ + fn new( + ast: &GenericSyntaxTree, + snap_shot: &'a S, + delta: SR::Share>, + generalisations: SR::Share>, + ) -> Option { + ast.get_expansion().map(move |(l, r)| { + let left_finder = GeneralisationFinder::new( + l.as_ref(), + snap_shot, + delta.clone(), + generalisations.clone(), + ) + .map(Box::new); + let right_finder = GeneralisationFinder::new( + r.as_ref(), + snap_shot, + delta.clone(), + generalisations.clone(), + ) + .map(Box::new); + Self { + generalisations, + snap_shot, + delta, + composition_id_iter: Box::new(empty()), + left_syntax: l, + right_syntax: r, + left_finder, + right_finder, + concepts_used: false, + } + }) + } +} + +impl< + 'a, + S: SnapShotReader, + CI: ConceptId + 'static, + SR: SharedReference, + > Iterator for GeneralisationFinder<'a, S, CI, SR> +{ + type Item = CI; + + fn next(&mut self) -> Option { + loop { + for id in self.composition_id_iter.by_ref() { + if self.generalisations.insert(id) { + return Some(id); + } + } + + // Need to replenish composition_id_iter + self.composition_id_iter = match ( + if self.concepts_used { + None + } else { + self.left_syntax + .get_concept() + .map(|c| { + self.snap_shot.read_concept(self.delta.as_ref(), c) + }) + .map(|l| l.into_iter_composition_ids(Hand::Left)) + }, + if self.concepts_used { + None + } else { + self.right_syntax + .get_concept() + .map(|c| { + self.snap_shot.read_concept(self.delta.as_ref(), c) + }) + .map(|r| r.into_iter_composition_ids(Hand::Right)) + }, + ) { + (Some(iter), None) | (None, Some(iter)) => { + self.concepts_used = true; + Box::new(iter) + }, + (Some(l_iter), Some(r_iter)) => { + self.concepts_used = true; + Box::new(l_iter.chain(r_iter)) + }, + (None, None) => { + self.concepts_used = true; + match ( + self.left_finder.as_deref_mut().and_then(|finder| { + let g = finder.next()?; + + let concept = self + .snap_shot + .read_concept(self.delta.as_ref(), g); + Some(concept.into_iter_composition_ids(Hand::Left)) + }), + self.right_finder.as_mut().and_then(|finder| { + finder.next().map(|g| { + self.snap_shot + .read_concept(self.delta.as_ref(), g) + .into_iter_composition_ids(Hand::Right) + }) + }), + ) { + (None, None) => return None, + (Some(iter), None) | (None, Some(iter)) => { + Box::new(iter) + }, + (Some(l_iter), Some(r_iter)) => { + Box::new(l_iter.chain(r_iter)) + }, + } + }, + }; + } + } +} #[derive(PartialEq, Debug, Eq)] pub enum Comparison {