From 280796ab17b9c41c3f978ce866e18bb0d7a5b5c5 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 2 Jan 2023 13:18:55 +0100 Subject: [PATCH] move type-system & context into separate module --- nested/src/char_editor.rs | 3 +- nested/src/core/mod.rs | 11 +- nested/src/integer/editor.rs | 3 +- nested/src/lib.rs | 4 +- nested/src/list/editor.rs | 3 +- nested/src/list/pty_editor.rs | 3 +- nested/src/make_editor.rs | 10 +- nested/src/product/editor.rs | 3 +- nested/src/product/nav.rs | 2 +- nested/src/product/segment.rs | 3 +- nested/src/tree/node.rs | 6 +- nested/src/{core => type_system}/context.rs | 203 +---------------- nested/src/type_system/mod.rs | 10 + nested/src/type_system/repr_tree.rs | 205 ++++++++++++++++++ nested/src/{core => type_system}/type_term.rs | 0 nested/src/type_term_editor.rs | 3 +- shell/src/main.rs | 13 +- 17 files changed, 260 insertions(+), 225 deletions(-) rename nested/src/{core => type_system}/context.rs (52%) create mode 100644 nested/src/type_system/mod.rs create mode 100644 nested/src/type_system/repr_tree.rs rename nested/src/{core => type_system}/type_term.rs (100%) diff --git a/nested/src/char_editor.rs b/nested/src/char_editor.rs index 89a92e9..8a1e22d 100644 --- a/nested/src/char_editor.rs +++ b/nested/src/char_editor.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, Context}, + core::{OuterViewPort}, + type_system::{Context}, singleton::{SingletonBuffer, SingletonView}, terminal::{TerminalAtom, TerminalEvent, TerminalStyle}, tree::NestedNode, Commander diff --git a/nested/src/core/mod.rs b/nested/src/core/mod.rs index 18c63a9..fb89afb 100644 --- a/nested/src/core/mod.rs +++ b/nested/src/core/mod.rs @@ -1,17 +1,12 @@ pub mod channel; -pub mod context; pub mod observer; pub mod port; -pub mod type_term; pub mod view; pub use { channel::{queue_channel, set_channel, singleton_channel, ChannelReceiver, ChannelSender}, - context::{Context, MorphismMode, MorphismType, ReprTree}, observer::{NotifyFnObserver, Observer, ObserverBroadcast, ObserverExt, ResetFnObserver}, - port::{ - AnyInnerViewPort, AnyOuterViewPort, AnyViewPort, InnerViewPort, OuterViewPort, ViewPort, - }, - type_term::{TypeDict, TypeID, TypeTerm, TypeLadder}, - view::View, + port::{AnyInnerViewPort, AnyOuterViewPort, AnyViewPort, InnerViewPort, OuterViewPort, ViewPort}, + view::View }; + diff --git a/nested/src/integer/editor.rs b/nested/src/integer/editor.rs index ccc6307..6d99f57 100644 --- a/nested/src/integer/editor.rs +++ b/nested/src/integer/editor.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, Context, TypeTerm}, + core::{OuterViewPort}, + type_system::{Context, TypeTerm}, list::{PTYListEditor}, sequence::{SequenceView, SequenceViewExt, decorator::{PTYSeqDecorate, SeqDecorStyle}}, singleton::{SingletonBuffer, SingletonView}, diff --git a/nested/src/lib.rs b/nested/src/lib.rs index afcd3dc..0ed80a3 100644 --- a/nested/src/lib.rs +++ b/nested/src/lib.rs @@ -2,11 +2,13 @@ // general pub mod core; +pub mod type_system; pub mod projection; pub mod bimap; pub mod modulo; pub use modulo::modulo; + // semantics pub mod singleton; pub mod sequence; @@ -45,7 +47,7 @@ pub trait Commander { use std::sync::{Arc, RwLock}; use crate::{ - core::context::ReprTree, + type_system::ReprTree, singleton::SingletonView }; diff --git a/nested/src/list/editor.rs b/nested/src/list/editor.rs index d97e883..6f38e2e 100644 --- a/nested/src/list/editor.rs +++ b/nested/src/list/editor.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, ViewPort, Context, TypeTerm}, + core::{OuterViewPort, ViewPort}, + type_system::{Context, TypeTerm}, list::{ ListCursor, ListSegment, diff --git a/nested/src/list/pty_editor.rs b/nested/src/list/pty_editor.rs index c85c43f..cc499c3 100644 --- a/nested/src/list/pty_editor.rs +++ b/nested/src/list/pty_editor.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, Context, TypeTerm}, + core::{OuterViewPort}, + type_system::{Context, TypeTerm}, list::{ ListCursor, ListCursorMode, ListEditor diff --git a/nested/src/make_editor.rs b/nested/src/make_editor.rs index 1425edb..ee7378b 100644 --- a/nested/src/make_editor.rs +++ b/nested/src/make_editor.rs @@ -1,6 +1,6 @@ use { crate::{ - core::{TypeTerm, Context}, + type_system::{TypeTerm, Context}, integer::{DigitEditor, PosIntEditor}, list::{PTYListEditor}, sequence::{decorator::{SeqDecorStyle}}, @@ -12,6 +12,14 @@ use { std::sync::{Arc, RwLock}, }; +pub fn init_mem_ctx(parent: Arc>) -> Arc> { + let ctx = Arc::new(RwLock::new(Context::with_parent(Some(parent)))); + + ctx.write().unwrap().add_typename("Vec".into()); + + ctx +} + pub fn init_editor_ctx(parent: Arc>) -> Arc> { let ctx = Arc::new(RwLock::new(Context::with_parent(Some(parent)))); diff --git a/nested/src/product/editor.rs b/nested/src/product/editor.rs index be50901..4ea4bbb 100644 --- a/nested/src/product/editor.rs +++ b/nested/src/product/editor.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, TypeLadder, Context}, + core::{OuterViewPort}, + type_system::{TypeLadder, Context}, terminal::{ TerminalEditor, TerminalEditorResult, TerminalEvent, TerminalView diff --git a/nested/src/product/nav.rs b/nested/src/product/nav.rs index 1e8ce9d..01456e4 100644 --- a/nested/src/product/nav.rs +++ b/nested/src/product/nav.rs @@ -1,6 +1,6 @@ use { crate::{ - core::Context, + type_system::Context, list::ListCursorMode, tree::{TreeNav, TreeNavResult, TreeCursor}, product::{segment::ProductEditorSegment, ProductEditor}, diff --git a/nested/src/product/segment.rs b/nested/src/product/segment.rs index 395755c..30d4851 100644 --- a/nested/src/product/segment.rs +++ b/nested/src/product/segment.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, TypeLadder, Context}, + core::{OuterViewPort}, + type_system::{TypeLadder, Context}, terminal::{ TerminalStyle, TerminalView, make_label diff --git a/nested/src/tree/node.rs b/nested/src/tree/node.rs index 35652da..07a3edb 100644 --- a/nested/src/tree/node.rs +++ b/nested/src/tree/node.rs @@ -2,7 +2,8 @@ use { std::sync::{Arc, RwLock}, cgmath::Vector2, crate::{ - core::{ViewPort, OuterViewPort, AnyOuterViewPort, context::ReprTree, Context}, + core::{ViewPort, OuterViewPort, AnyOuterViewPort}, + type_system::{ReprTree, Context}, singleton::{SingletonBuffer}, sequence::SequenceView, terminal::{TerminalView, TerminalEvent, TerminalEditor, TerminalEditorResult}, @@ -16,6 +17,8 @@ use { #[derive(Clone)] pub struct NestedNode { pub ctx: Option>>, + +// pub abs: Option>>, pub view: Option>, pub diag: Option>>, pub cmd: Option>>, @@ -50,7 +53,6 @@ impl TerminalEditor for NestedNode { } } - impl TreeNav for NestedNode { fn get_cursor(&self) -> TreeCursor { if let Some(tn) = self.tree_nav.as_ref() { diff --git a/nested/src/core/context.rs b/nested/src/type_system/context.rs similarity index 52% rename from nested/src/core/context.rs rename to nested/src/type_system/context.rs index 3d463e8..779d0e6 100644 --- a/nested/src/core/context.rs +++ b/nested/src/type_system/context.rs @@ -1,214 +1,17 @@ use { crate::{ - core::{ - type_term::{TypeDict, TypeTerm, TypeID}, - AnyOuterViewPort, OuterViewPort, View, - }, + core::{AnyOuterViewPort, OuterViewPort, View}, + type_system::{TypeDict, TypeTerm, TypeID, ReprTree}, tree::NestedNode }, std::{ collections::HashMap, sync::{Arc, RwLock}, - }, + } }; //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> -#[derive(Clone)] -pub struct ReprTree { - type_tag: TypeTerm, - port: Option, - branches: HashMap>>, -} - -impl ReprTree { - pub fn new(type_tag: TypeTerm) -> Self { - ReprTree { - type_tag, - port: None, - branches: HashMap::new(), - } - } - - pub fn new_leaf(type_tag: TypeTerm, port: AnyOuterViewPort) -> Arc> { - let mut tree = ReprTree::new(type_tag); - tree.insert_leaf(vec![].into_iter(), port); - Arc::new(RwLock::new(tree)) - } - - pub fn insert_branch(&mut self, repr: Arc>) { - self.branches.insert(repr.clone().read().unwrap().type_tag.clone(), repr.clone()); - } - - pub fn insert_leaf( - &mut self, - mut type_ladder: impl Iterator, - port: AnyOuterViewPort, - ) { - if let Some(type_term) = type_ladder.next() { - if let Some(next_repr) = self.branches.get(&type_term) { - next_repr.write().unwrap().insert_leaf(type_ladder, port); - } else { - let mut next_repr = ReprTree::new(type_term.clone()); - next_repr.insert_leaf(type_ladder, port); - self.insert_branch(Arc::new(RwLock::new(next_repr))); - } - } else { - self.port = Some(port); - } - } - - //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - - pub fn get_port(&self) -> Option> - where - V::Msg: Clone, - { - Some( - self.port - .clone()? - .downcast::() - .ok() - .unwrap() - ) - } - - pub fn get_view(&self) -> Option> - where - V::Msg: Clone, - { - self.get_port::()? - .get_view() - } - - // descend - pub fn downcast(&self, dst_type: &TypeTerm) -> Option>> { - self.branches.get(dst_type).cloned() - } - - pub fn downcast_ladder(&self, mut repr_ladder: impl Iterator) -> Option>> { - let first = repr_ladder.next()?; - repr_ladder.fold( - self.downcast(&first), - |s, t| s?.read().unwrap().downcast(&t)) - } - - // ascend - pub fn upcast(rt: &Arc>, type_term: TypeTerm) -> Arc> { - let mut n = Self::new(type_term); - n.insert_branch(rt.clone()); - Arc::new(RwLock::new(n)) - } - -/* - pub fn add_iso_repr( - &self, - type_ladder: impl Iterator, - morphism_constructors: &HashMap Object>>, - ) { - let mut cur_repr = self.repr.clone(); - - for dst_type in type_ladder { - if let Some(next_repr) = self.repr.read().unwrap().branches.get(&dst_type) { - // go deeper - cur_repr = next_repr.clone(); - } else { - // search for morphism constructor and insert new repr - let mut obj = None; - - for src_type in cur_repr.read().unwrap().branches.keys() { - if let Some(ctor) = morphism_constructors.get(&MorphismType { - mode: MorphismMode::Iso, - src_type: src_type.clone(), - dst_type: dst_type.clone(), - }) { - let new_obj = ctor(Object { - type_tag: src_type.clone(), - repr: cur_repr - .read() - .unwrap() - .branches - .get(&src_type) - .unwrap() - .clone(), - }); - - assert!(new_obj.type_tag == dst_type); - - obj = Some(new_obj); - break; - } - } - - if let Some(obj) = obj { - cur_repr - .write() - .unwrap() - .insert_branch(obj.type_tag, obj.repr); - } else { - panic!("could not find matching isomorphism!"); - } - } - } - } - - pub fn add_mono_repr<'a>( - &self, - type_ladder: impl Iterator, - morphism_constructors: &HashMap Object>>, - ) { - let mut cur_type = self.type_tag.clone(); - let mut cur_repr = self.repr.clone(); - - for dst_type in type_ladder { - if let Some(next_repr) = self.repr.read().unwrap().branches.get(&dst_type) { - // go deeper - cur_type = dst_type; - cur_repr = next_repr.clone(); - } else { - if let Some(constructor) = morphism_constructors.get(&MorphismType { - mode: MorphismMode::Mono, - src_type: cur_type.clone(), - dst_type: dst_type.clone(), - }) { - let new_obj = constructor(Object { - type_tag: cur_type.clone(), - repr: cur_repr - .read() - .unwrap() - .branches - .get(&cur_type) - .unwrap() - .clone(), - }); - - assert!(new_obj.type_tag == dst_type); - cur_repr - .write() - .unwrap() - .insert_branch(new_obj.type_tag.clone(), new_obj.repr.clone()); - - cur_type = new_obj.type_tag; - cur_repr = new_obj.repr; - } - } - } - } - - // replace with higher-level type in which self is a repr branch - pub fn epi_cast<'a>( - &self, - _type_ladder: impl Iterator, - _morphism_constructors: &HashMap Object>>, - ) { - // todo - -} - */ -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - pub struct TypeLadder(Vec); #[derive(Clone, Copy, Hash, PartialEq, Eq)] diff --git a/nested/src/type_system/mod.rs b/nested/src/type_system/mod.rs new file mode 100644 index 0000000..72e2db3 --- /dev/null +++ b/nested/src/type_system/mod.rs @@ -0,0 +1,10 @@ +pub mod type_term; +pub mod repr_tree; +pub mod context; + +pub use { + repr_tree::{ReprTree}, + type_term::{TypeDict, TypeID, TypeTerm, TypeLadder}, + context::{Context, MorphismMode, MorphismType}, +}; + diff --git a/nested/src/type_system/repr_tree.rs b/nested/src/type_system/repr_tree.rs new file mode 100644 index 0000000..cd1d046 --- /dev/null +++ b/nested/src/type_system/repr_tree.rs @@ -0,0 +1,205 @@ +use { + crate::{ + core::{AnyOuterViewPort, OuterViewPort, View}, + type_system::{TypeDict, TypeTerm, TypeID}, + tree::NestedNode + }, + std::{ + collections::HashMap, + sync::{Arc, RwLock}, + }, +}; + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + +#[derive(Clone)] +pub struct ReprTree { + type_tag: TypeTerm, + port: Option, + branches: HashMap>>, +} + +impl ReprTree { + pub fn new(type_tag: TypeTerm) -> Self { + ReprTree { + type_tag, + port: None, + branches: HashMap::new(), + } + } + + pub fn new_leaf(type_tag: TypeTerm, port: AnyOuterViewPort) -> Arc> { + let mut tree = ReprTree::new(type_tag); + tree.insert_leaf(vec![].into_iter(), port); + Arc::new(RwLock::new(tree)) + } + + pub fn insert_branch(&mut self, repr: Arc>) { + self.branches.insert(repr.clone().read().unwrap().type_tag.clone(), repr.clone()); + } + + pub fn insert_leaf( + &mut self, + mut type_ladder: impl Iterator, + port: AnyOuterViewPort, + ) { + if let Some(type_term) = type_ladder.next() { + if let Some(next_repr) = self.branches.get(&type_term) { + next_repr.write().unwrap().insert_leaf(type_ladder, port); + } else { + let mut next_repr = ReprTree::new(type_term.clone()); + next_repr.insert_leaf(type_ladder, port); + self.insert_branch(Arc::new(RwLock::new(next_repr))); + } + } else { + self.port = Some(port); + } + } + + //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + + pub fn get_port(&self) -> Option> + where + V::Msg: Clone, + { + Some( + self.port + .clone()? + .downcast::() + .ok() + .unwrap() + ) + } + + pub fn get_view(&self) -> Option> + where + V::Msg: Clone, + { + self.get_port::()? + .get_view() + } + + pub fn descend(&self, dst_type: &TypeTerm) -> Option>> { + self.branches.get(dst_type).cloned() + } + + pub fn descend_ladder(&self, mut repr_ladder: impl Iterator) -> Option>> { + let first = repr_ladder.next()?; + repr_ladder.fold( + self.descend(&first), + |s, t| s?.read().unwrap().descend(&t)) + } + + pub fn ascend(rt: &Arc>, type_term: TypeTerm) -> Arc> { + let mut n = Self::new(type_term); + n.insert_branch(rt.clone()); + Arc::new(RwLock::new(n)) + } + +/* + pub fn add_iso_repr( + &self, + type_ladder: impl Iterator, + morphism_constructors: &HashMap Object>>, + ) { + let mut cur_repr = self.repr.clone(); + + for dst_type in type_ladder { + if let Some(next_repr) = self.repr.read().unwrap().branches.get(&dst_type) { + // go deeper + cur_repr = next_repr.clone(); + } else { + // search for morphism constructor and insert new repr + let mut obj = None; + + for src_type in cur_repr.read().unwrap().branches.keys() { + if let Some(ctor) = morphism_constructors.get(&MorphismType { + mode: MorphismMode::Iso, + src_type: src_type.clone(), + dst_type: dst_type.clone(), + }) { + let new_obj = ctor(Object { + type_tag: src_type.clone(), + repr: cur_repr + .read() + .unwrap() + .branches + .get(&src_type) + .unwrap() + .clone(), + }); + + assert!(new_obj.type_tag == dst_type); + + obj = Some(new_obj); + break; + } + } + + if let Some(obj) = obj { + cur_repr + .write() + .unwrap() + .insert_branch(obj.type_tag, obj.repr); + } else { + panic!("could not find matching isomorphism!"); + } + } + } + } + + pub fn add_mono_repr<'a>( + &self, + type_ladder: impl Iterator, + morphism_constructors: &HashMap Object>>, + ) { + let mut cur_type = self.type_tag.clone(); + let mut cur_repr = self.repr.clone(); + + for dst_type in type_ladder { + if let Some(next_repr) = self.repr.read().unwrap().branches.get(&dst_type) { + // go deeper + cur_type = dst_type; + cur_repr = next_repr.clone(); + } else { + if let Some(constructor) = morphism_constructors.get(&MorphismType { + mode: MorphismMode::Mono, + src_type: cur_type.clone(), + dst_type: dst_type.clone(), + }) { + let new_obj = constructor(Object { + type_tag: cur_type.clone(), + repr: cur_repr + .read() + .unwrap() + .branches + .get(&cur_type) + .unwrap() + .clone(), + }); + + assert!(new_obj.type_tag == dst_type); + cur_repr + .write() + .unwrap() + .insert_branch(new_obj.type_tag.clone(), new_obj.repr.clone()); + + cur_type = new_obj.type_tag; + cur_repr = new_obj.repr; + } + } + } + } + + // replace with higher-level type in which self is a repr branch + pub fn epi_cast<'a>( + &self, + _type_ladder: impl Iterator, + _morphism_constructors: &HashMap Object>>, + ) { + // todo + +} + */ +} + diff --git a/nested/src/core/type_term.rs b/nested/src/type_system/type_term.rs similarity index 100% rename from nested/src/core/type_term.rs rename to nested/src/type_system/type_term.rs diff --git a/nested/src/type_term_editor.rs b/nested/src/type_term_editor.rs index 19c555a..87eb5b9 100644 --- a/nested/src/type_term_editor.rs +++ b/nested/src/type_term_editor.rs @@ -1,6 +1,7 @@ use { crate::{ - core::{OuterViewPort, Context}, + core::{OuterViewPort}, + type_system::{Context}, terminal::{TerminalEvent, TerminalView, TerminalEditor, TerminalEditorResult}, sequence::{SequenceView, decorator::SeqDecorStyle}, list::{PTYListEditor}, diff --git a/shell/src/main.rs b/shell/src/main.rs index 0cf823e..b1c56c5 100644 --- a/shell/src/main.rs +++ b/shell/src/main.rs @@ -9,7 +9,8 @@ mod pty; use { cgmath::{Point2, Vector2}, nested::{ - core::{port::UpdateTask, Observer, AnyOuterViewPort, ViewPort, Context, ReprTree}, + core::{port::UpdateTask, Observer, AnyOuterViewPort, ViewPort}, + type_system::{Context, ReprTree}, index::IndexArea, list::{ListCursorMode, PTYListEditor}, sequence::{decorator::{SeqDecorStyle, Separate}}, @@ -54,19 +55,21 @@ async fn main() { // Type Context // let ctx = Arc::new(RwLock::new(Context::new())); + let ctx = nested::make_editor::init_mem_ctx(ctx); let ctx = nested::make_editor::init_editor_ctx(ctx); let ctx = nested::make_editor::init_math_ctx(ctx); let ctx = nested::make_editor::init_os_ctx(ctx); let vb = VecBuffer::::new(); let rt_char = ReprTree::new_leaf( - ctx.read().unwrap().type_term_from_str("( List Char 0 )").unwrap(), + ctx.read().unwrap().type_term_from_str("( Vec Char )").unwrap(), AnyOuterViewPort::from(vb.get_port()) ); - let rt_digit = ReprTree::upcast(&rt_char, ctx.read().unwrap().type_term_from_str("( List ( Digit 10 ) )").unwrap()); + + let rt_digit = ReprTree::ascend(&rt_char, ctx.read().unwrap().type_term_from_str("( List ( Digit 10 ) )").unwrap()); rt_digit.write().unwrap().insert_branch( ReprTree::new_leaf( - ctx.read().unwrap().type_term_from_str("( List MachineInt )").unwrap(), + ctx.read().unwrap().type_term_from_str("( Vec MachineInt )").unwrap(), AnyOuterViewPort::from( vb.get_port().to_sequence().map( |c: &char| { @@ -76,7 +79,7 @@ async fn main() { ) ) ); - + /* ctx.write().unwrap().add_morphism( MorphismType{