From d02f33ee177958631ede178a41f0f73db6550db6 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 30 May 2024 23:35:54 +0200 Subject: [PATCH] ReprTree: add halo type --- lib-nested-core/src/repr_tree/mod.rs | 55 ++++++++++++++++++-------- lib-nested-core/src/repr_tree/tests.rs | 24 +++++++++++ 2 files changed, 63 insertions(+), 16 deletions(-) diff --git a/lib-nested-core/src/repr_tree/mod.rs b/lib-nested-core/src/repr_tree/mod.rs index 55c74ec..13c3daa 100644 --- a/lib-nested-core/src/repr_tree/mod.rs +++ b/lib-nested-core/src/repr_tree/mod.rs @@ -44,6 +44,7 @@ pub struct ReprLeaf { #[derive(Clone)] pub struct ReprTree { + halo: TypeTerm, type_tag: TypeTerm, branches: HashMap>>, leaf: Option< ReprLeaf > @@ -207,8 +208,13 @@ impl ReprLeaf { impl ReprTree { pub fn new(type_tag: impl Into) -> Self { + let type_tag = type_tag.into(); + + assert!(type_tag.is_flat()); + ReprTree { - type_tag: type_tag.into(), + halo: TypeTerm::unit(), + type_tag: type_tag.clone(), branches: HashMap::new(), leaf: None } @@ -222,8 +228,31 @@ impl ReprTree { &self.type_tag } + pub fn set_halo(&mut self, halo_type: impl Into) { + self.halo = halo_type.into(); + for (branch_type, branch) in self.branches.iter() { + branch.write().unwrap().set_halo( TypeTerm::Ladder(vec![ + self.halo.clone(), + self.type_tag.clone() + ]).normalize() + ); + } + } + + pub fn get_halo_type(&self) -> &TypeTerm { + &self.halo + } + pub fn insert_branch(&mut self, repr: Arc>) { - self.branches.insert(repr.clone().read().unwrap().type_tag.clone(), repr.clone()); + let branch_type = repr.read().unwrap().get_type().clone(); + + assert!(branch_type.is_flat()); + + repr.write().unwrap().set_halo( TypeTerm::Ladder(vec![ + self.halo.clone(), + self.type_tag.clone() + ]).normalize() ); + self.branches.insert(branch_type, repr.clone()); } pub fn from_char(ctx: &Arc>, c: char ) -> Arc> { @@ -250,7 +279,6 @@ impl ReprTree { Arc::new(RwLock::new(rt)) } - pub fn from_vec_buffer( type_tag: impl Into, buf: VecBuffer ) -> Arc> where T: Clone + Send + Sync + 'static { @@ -437,21 +465,16 @@ impl ReprTreeExt for Arc> { } fn create_branch(&mut self, rung: impl Into) { - let lnf = rung.into().get_lnf_vec(); - eprintln!("lnf ={:?}",lnf); + let mut lnf = rung.into().get_lnf_vec().into_iter(); + if let Some(rung) = lnf.next() { + let mut parent = ReprTree::new_arc( rung ); + self.insert_branch( parent.clone() ); - let mut child = None; - for rung in lnf.iter().rev() { - eprintln!("create {:?}",rung); - let mut parent = ReprTree::new_arc( rung.clone() ); - if let Some(c) = child.take() { - parent.insert_branch( c ); + for rung in lnf { + let r = ReprTree::new_arc( rung ); + parent.insert_branch(r.clone()); + parent = r; } - child = Some(parent); - } - - if let Some(child) = child.take() { - self.insert_branch(child); } } diff --git a/lib-nested-core/src/repr_tree/tests.rs b/lib-nested-core/src/repr_tree/tests.rs index 4970d06..4e6aa21 100644 --- a/lib-nested-core/src/repr_tree/tests.rs +++ b/lib-nested-core/src/repr_tree/tests.rs @@ -12,6 +12,30 @@ use { std::sync::{Arc, RwLock} }; +#[test] +fn halo_type() { + let ctx = Arc::new(RwLock::new(Context::new())); + + let mut rt1 = ReprTree::new_arc(Context::parse(&ctx, "ℕ")); + let mut rt2 = ReprTree::new_arc(Context::parse(&ctx, "")); + rt1.insert_branch( rt2.clone() ); + assert_eq!( rt2.read().unwrap().get_halo_type(), &Context::parse(&ctx, "ℕ") ); + + let mut rt3 = ReprTree::new_arc(Context::parse(&ctx, ">")); + rt2.insert_branch( rt3.clone() ); + assert_eq!( rt3.read().unwrap().get_halo_type(), &Context::parse(&ctx, "ℕ~") ); + + let rt4 = ReprTree::new_arc(Context::parse(&ctx, ">")); + rt3.insert_branch( rt4.clone() ); + assert_eq!( rt4.read().unwrap().get_halo_type(), &Context::parse(&ctx, "ℕ~~>") ); + + + let mut r = ReprTree::new_arc(Context::parse(&ctx, "ℕ")); + r.create_branch(Context::parse(&ctx, "~>")); + assert_eq!( r.descend(Context::parse(&ctx, "")).unwrap().read().unwrap().get_halo_type(), &Context::parse(&ctx, "ℕ") ); + assert_eq!( r.descend(Context::parse(&ctx, "~>")).unwrap().read().unwrap().get_halo_type(), &Context::parse(&ctx, "ℕ~") ); +} + #[test] fn char_view() { let ctx = Arc::new(RwLock::new(Context::new()));