move type-system & context into separate module
This commit is contained in:
parent
97000cab7a
commit
280796ab17
17 changed files with 260 additions and 225 deletions
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, Context},
|
core::{OuterViewPort},
|
||||||
|
type_system::{Context},
|
||||||
singleton::{SingletonBuffer, SingletonView},
|
singleton::{SingletonBuffer, SingletonView},
|
||||||
terminal::{TerminalAtom, TerminalEvent, TerminalStyle},
|
terminal::{TerminalAtom, TerminalEvent, TerminalStyle},
|
||||||
tree::NestedNode, Commander
|
tree::NestedNode, Commander
|
||||||
|
|
|
@ -1,17 +1,12 @@
|
||||||
pub mod channel;
|
pub mod channel;
|
||||||
pub mod context;
|
|
||||||
pub mod observer;
|
pub mod observer;
|
||||||
pub mod port;
|
pub mod port;
|
||||||
pub mod type_term;
|
|
||||||
pub mod view;
|
pub mod view;
|
||||||
|
|
||||||
pub use {
|
pub use {
|
||||||
channel::{queue_channel, set_channel, singleton_channel, ChannelReceiver, ChannelSender},
|
channel::{queue_channel, set_channel, singleton_channel, ChannelReceiver, ChannelSender},
|
||||||
context::{Context, MorphismMode, MorphismType, ReprTree},
|
|
||||||
observer::{NotifyFnObserver, Observer, ObserverBroadcast, ObserverExt, ResetFnObserver},
|
observer::{NotifyFnObserver, Observer, ObserverBroadcast, ObserverExt, ResetFnObserver},
|
||||||
port::{
|
port::{AnyInnerViewPort, AnyOuterViewPort, AnyViewPort, InnerViewPort, OuterViewPort, ViewPort},
|
||||||
AnyInnerViewPort, AnyOuterViewPort, AnyViewPort, InnerViewPort, OuterViewPort, ViewPort,
|
view::View
|
||||||
},
|
|
||||||
type_term::{TypeDict, TypeID, TypeTerm, TypeLadder},
|
|
||||||
view::View,
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, Context, TypeTerm},
|
core::{OuterViewPort},
|
||||||
|
type_system::{Context, TypeTerm},
|
||||||
list::{PTYListEditor},
|
list::{PTYListEditor},
|
||||||
sequence::{SequenceView, SequenceViewExt, decorator::{PTYSeqDecorate, SeqDecorStyle}},
|
sequence::{SequenceView, SequenceViewExt, decorator::{PTYSeqDecorate, SeqDecorStyle}},
|
||||||
singleton::{SingletonBuffer, SingletonView},
|
singleton::{SingletonBuffer, SingletonView},
|
||||||
|
|
|
@ -2,11 +2,13 @@
|
||||||
|
|
||||||
// general
|
// general
|
||||||
pub mod core;
|
pub mod core;
|
||||||
|
pub mod type_system;
|
||||||
pub mod projection;
|
pub mod projection;
|
||||||
pub mod bimap;
|
pub mod bimap;
|
||||||
pub mod modulo;
|
pub mod modulo;
|
||||||
pub use modulo::modulo;
|
pub use modulo::modulo;
|
||||||
|
|
||||||
|
|
||||||
// semantics
|
// semantics
|
||||||
pub mod singleton;
|
pub mod singleton;
|
||||||
pub mod sequence;
|
pub mod sequence;
|
||||||
|
@ -45,7 +47,7 @@ pub trait Commander {
|
||||||
|
|
||||||
use std::sync::{Arc, RwLock};
|
use std::sync::{Arc, RwLock};
|
||||||
use crate::{
|
use crate::{
|
||||||
core::context::ReprTree,
|
type_system::ReprTree,
|
||||||
singleton::SingletonView
|
singleton::SingletonView
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, ViewPort, Context, TypeTerm},
|
core::{OuterViewPort, ViewPort},
|
||||||
|
type_system::{Context, TypeTerm},
|
||||||
list::{
|
list::{
|
||||||
ListCursor,
|
ListCursor,
|
||||||
ListSegment,
|
ListSegment,
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, Context, TypeTerm},
|
core::{OuterViewPort},
|
||||||
|
type_system::{Context, TypeTerm},
|
||||||
list::{
|
list::{
|
||||||
ListCursor, ListCursorMode,
|
ListCursor, ListCursorMode,
|
||||||
ListEditor
|
ListEditor
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{TypeTerm, Context},
|
type_system::{TypeTerm, Context},
|
||||||
integer::{DigitEditor, PosIntEditor},
|
integer::{DigitEditor, PosIntEditor},
|
||||||
list::{PTYListEditor},
|
list::{PTYListEditor},
|
||||||
sequence::{decorator::{SeqDecorStyle}},
|
sequence::{decorator::{SeqDecorStyle}},
|
||||||
|
@ -12,6 +12,14 @@ use {
|
||||||
std::sync::{Arc, RwLock},
|
std::sync::{Arc, RwLock},
|
||||||
};
|
};
|
||||||
|
|
||||||
|
pub fn init_mem_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
|
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
let ctx = Arc::new(RwLock::new(Context::with_parent(Some(parent))));
|
let ctx = Arc::new(RwLock::new(Context::with_parent(Some(parent))));
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, TypeLadder, Context},
|
core::{OuterViewPort},
|
||||||
|
type_system::{TypeLadder, Context},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalEditor, TerminalEditorResult,
|
TerminalEditor, TerminalEditorResult,
|
||||||
TerminalEvent, TerminalView
|
TerminalEvent, TerminalView
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::Context,
|
type_system::Context,
|
||||||
list::ListCursorMode,
|
list::ListCursorMode,
|
||||||
tree::{TreeNav, TreeNavResult, TreeCursor},
|
tree::{TreeNav, TreeNavResult, TreeCursor},
|
||||||
product::{segment::ProductEditorSegment, ProductEditor},
|
product::{segment::ProductEditorSegment, ProductEditor},
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, TypeLadder, Context},
|
core::{OuterViewPort},
|
||||||
|
type_system::{TypeLadder, Context},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalStyle, TerminalView,
|
TerminalStyle, TerminalView,
|
||||||
make_label
|
make_label
|
||||||
|
|
|
@ -2,7 +2,8 @@ use {
|
||||||
std::sync::{Arc, RwLock},
|
std::sync::{Arc, RwLock},
|
||||||
cgmath::Vector2,
|
cgmath::Vector2,
|
||||||
crate::{
|
crate::{
|
||||||
core::{ViewPort, OuterViewPort, AnyOuterViewPort, context::ReprTree, Context},
|
core::{ViewPort, OuterViewPort, AnyOuterViewPort},
|
||||||
|
type_system::{ReprTree, Context},
|
||||||
singleton::{SingletonBuffer},
|
singleton::{SingletonBuffer},
|
||||||
sequence::SequenceView,
|
sequence::SequenceView,
|
||||||
terminal::{TerminalView, TerminalEvent, TerminalEditor, TerminalEditorResult},
|
terminal::{TerminalView, TerminalEvent, TerminalEditor, TerminalEditorResult},
|
||||||
|
@ -16,6 +17,8 @@ use {
|
||||||
#[derive(Clone)]
|
#[derive(Clone)]
|
||||||
pub struct NestedNode {
|
pub struct NestedNode {
|
||||||
pub ctx: Option<Arc<RwLock<Context>>>,
|
pub ctx: Option<Arc<RwLock<Context>>>,
|
||||||
|
|
||||||
|
// pub abs: Option<Arc<RwLock<ReprTree>>>,
|
||||||
pub view: Option<OuterViewPort<dyn TerminalView>>,
|
pub view: Option<OuterViewPort<dyn TerminalView>>,
|
||||||
pub diag: Option<OuterViewPort<dyn SequenceView<Item = Message>>>,
|
pub diag: Option<OuterViewPort<dyn SequenceView<Item = Message>>>,
|
||||||
pub cmd: Option<Arc<RwLock<dyn ObjCommander + Send + Sync>>>,
|
pub cmd: Option<Arc<RwLock<dyn ObjCommander + Send + Sync>>>,
|
||||||
|
@ -50,7 +53,6 @@ impl TerminalEditor for NestedNode {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
impl TreeNav for NestedNode {
|
impl TreeNav for NestedNode {
|
||||||
fn get_cursor(&self) -> TreeCursor {
|
fn get_cursor(&self) -> TreeCursor {
|
||||||
if let Some(tn) = self.tree_nav.as_ref() {
|
if let Some(tn) = self.tree_nav.as_ref() {
|
||||||
|
|
|
@ -1,214 +1,17 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{
|
core::{AnyOuterViewPort, OuterViewPort, View},
|
||||||
type_term::{TypeDict, TypeTerm, TypeID},
|
type_system::{TypeDict, TypeTerm, TypeID, ReprTree},
|
||||||
AnyOuterViewPort, OuterViewPort, View,
|
|
||||||
},
|
|
||||||
tree::NestedNode
|
tree::NestedNode
|
||||||
},
|
},
|
||||||
std::{
|
std::{
|
||||||
collections::HashMap,
|
collections::HashMap,
|
||||||
sync::{Arc, RwLock},
|
sync::{Arc, RwLock},
|
||||||
},
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
#[derive(Clone)]
|
|
||||||
pub struct ReprTree {
|
|
||||||
type_tag: TypeTerm,
|
|
||||||
port: Option<AnyOuterViewPort>,
|
|
||||||
branches: HashMap<TypeTerm, Arc<RwLock<ReprTree>>>,
|
|
||||||
}
|
|
||||||
|
|
||||||
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<RwLock<Self>> {
|
|
||||||
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<RwLock<ReprTree>>) {
|
|
||||||
self.branches.insert(repr.clone().read().unwrap().type_tag.clone(), repr.clone());
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn insert_leaf(
|
|
||||||
&mut self,
|
|
||||||
mut type_ladder: impl Iterator<Item = TypeTerm>,
|
|
||||||
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<V: View + ?Sized + 'static>(&self) -> Option<OuterViewPort<V>>
|
|
||||||
where
|
|
||||||
V::Msg: Clone,
|
|
||||||
{
|
|
||||||
Some(
|
|
||||||
self.port
|
|
||||||
.clone()?
|
|
||||||
.downcast::<V>()
|
|
||||||
.ok()
|
|
||||||
.unwrap()
|
|
||||||
)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_view<V: View + ?Sized + 'static>(&self) -> Option<Arc<V>>
|
|
||||||
where
|
|
||||||
V::Msg: Clone,
|
|
||||||
{
|
|
||||||
self.get_port::<V>()?
|
|
||||||
.get_view()
|
|
||||||
}
|
|
||||||
|
|
||||||
// descend
|
|
||||||
pub fn downcast(&self, dst_type: &TypeTerm) -> Option<Arc<RwLock<ReprTree>>> {
|
|
||||||
self.branches.get(dst_type).cloned()
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn downcast_ladder(&self, mut repr_ladder: impl Iterator<Item = TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
|
||||||
let first = repr_ladder.next()?;
|
|
||||||
repr_ladder.fold(
|
|
||||||
self.downcast(&first),
|
|
||||||
|s, t| s?.read().unwrap().downcast(&t))
|
|
||||||
}
|
|
||||||
|
|
||||||
// ascend
|
|
||||||
pub fn upcast(rt: &Arc<RwLock<Self>>, type_term: TypeTerm) -> Arc<RwLock<ReprTree>> {
|
|
||||||
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<Item = TypeTerm>,
|
|
||||||
morphism_constructors: &HashMap<MorphismType, Box<dyn Fn(Object) -> 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<Item = TypeTerm>,
|
|
||||||
morphism_constructors: &HashMap<MorphismType, Box<dyn Fn(Object) -> 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<Item = TypeTerm>,
|
|
||||||
_morphism_constructors: &HashMap<MorphismType, Box<dyn Fn(Object) -> Object>>,
|
|
||||||
) {
|
|
||||||
// todo
|
|
||||||
|
|
||||||
}
|
|
||||||
*/
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
pub struct TypeLadder(Vec<TypeTerm>);
|
pub struct TypeLadder(Vec<TypeTerm>);
|
||||||
|
|
||||||
#[derive(Clone, Copy, Hash, PartialEq, Eq)]
|
#[derive(Clone, Copy, Hash, PartialEq, Eq)]
|
10
nested/src/type_system/mod.rs
Normal file
10
nested/src/type_system/mod.rs
Normal file
|
@ -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},
|
||||||
|
};
|
||||||
|
|
205
nested/src/type_system/repr_tree.rs
Normal file
205
nested/src/type_system/repr_tree.rs
Normal file
|
@ -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<AnyOuterViewPort>,
|
||||||
|
branches: HashMap<TypeTerm, Arc<RwLock<ReprTree>>>,
|
||||||
|
}
|
||||||
|
|
||||||
|
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<RwLock<Self>> {
|
||||||
|
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<RwLock<ReprTree>>) {
|
||||||
|
self.branches.insert(repr.clone().read().unwrap().type_tag.clone(), repr.clone());
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn insert_leaf(
|
||||||
|
&mut self,
|
||||||
|
mut type_ladder: impl Iterator<Item = TypeTerm>,
|
||||||
|
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<V: View + ?Sized + 'static>(&self) -> Option<OuterViewPort<V>>
|
||||||
|
where
|
||||||
|
V::Msg: Clone,
|
||||||
|
{
|
||||||
|
Some(
|
||||||
|
self.port
|
||||||
|
.clone()?
|
||||||
|
.downcast::<V>()
|
||||||
|
.ok()
|
||||||
|
.unwrap()
|
||||||
|
)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn get_view<V: View + ?Sized + 'static>(&self) -> Option<Arc<V>>
|
||||||
|
where
|
||||||
|
V::Msg: Clone,
|
||||||
|
{
|
||||||
|
self.get_port::<V>()?
|
||||||
|
.get_view()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn descend(&self, dst_type: &TypeTerm) -> Option<Arc<RwLock<ReprTree>>> {
|
||||||
|
self.branches.get(dst_type).cloned()
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn descend_ladder(&self, mut repr_ladder: impl Iterator<Item = TypeTerm>) -> Option<Arc<RwLock<ReprTree>>> {
|
||||||
|
let first = repr_ladder.next()?;
|
||||||
|
repr_ladder.fold(
|
||||||
|
self.descend(&first),
|
||||||
|
|s, t| s?.read().unwrap().descend(&t))
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn ascend(rt: &Arc<RwLock<Self>>, type_term: TypeTerm) -> Arc<RwLock<ReprTree>> {
|
||||||
|
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<Item = TypeTerm>,
|
||||||
|
morphism_constructors: &HashMap<MorphismType, Box<dyn Fn(Object) -> 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<Item = TypeTerm>,
|
||||||
|
morphism_constructors: &HashMap<MorphismType, Box<dyn Fn(Object) -> 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<Item = TypeTerm>,
|
||||||
|
_morphism_constructors: &HashMap<MorphismType, Box<dyn Fn(Object) -> Object>>,
|
||||||
|
) {
|
||||||
|
// todo
|
||||||
|
|
||||||
|
}
|
||||||
|
*/
|
||||||
|
}
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
core::{OuterViewPort, Context},
|
core::{OuterViewPort},
|
||||||
|
type_system::{Context},
|
||||||
terminal::{TerminalEvent, TerminalView, TerminalEditor, TerminalEditorResult},
|
terminal::{TerminalEvent, TerminalView, TerminalEditor, TerminalEditorResult},
|
||||||
sequence::{SequenceView, decorator::SeqDecorStyle},
|
sequence::{SequenceView, decorator::SeqDecorStyle},
|
||||||
list::{PTYListEditor},
|
list::{PTYListEditor},
|
||||||
|
|
|
@ -9,7 +9,8 @@ mod pty;
|
||||||
use {
|
use {
|
||||||
cgmath::{Point2, Vector2},
|
cgmath::{Point2, Vector2},
|
||||||
nested::{
|
nested::{
|
||||||
core::{port::UpdateTask, Observer, AnyOuterViewPort, ViewPort, Context, ReprTree},
|
core::{port::UpdateTask, Observer, AnyOuterViewPort, ViewPort},
|
||||||
|
type_system::{Context, ReprTree},
|
||||||
index::IndexArea,
|
index::IndexArea,
|
||||||
list::{ListCursorMode, PTYListEditor},
|
list::{ListCursorMode, PTYListEditor},
|
||||||
sequence::{decorator::{SeqDecorStyle, Separate}},
|
sequence::{decorator::{SeqDecorStyle, Separate}},
|
||||||
|
@ -54,19 +55,21 @@ async fn main() {
|
||||||
|
|
||||||
// Type Context //
|
// Type Context //
|
||||||
let ctx = Arc::new(RwLock::new(Context::new()));
|
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_editor_ctx(ctx);
|
||||||
let ctx = nested::make_editor::init_math_ctx(ctx);
|
let ctx = nested::make_editor::init_math_ctx(ctx);
|
||||||
let ctx = nested::make_editor::init_os_ctx(ctx);
|
let ctx = nested::make_editor::init_os_ctx(ctx);
|
||||||
|
|
||||||
let vb = VecBuffer::<char>::new();
|
let vb = VecBuffer::<char>::new();
|
||||||
let rt_char = ReprTree::new_leaf(
|
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())
|
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(
|
rt_digit.write().unwrap().insert_branch(
|
||||||
ReprTree::new_leaf(
|
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(
|
AnyOuterViewPort::from(
|
||||||
vb.get_port().to_sequence().map(
|
vb.get_port().to_sequence().map(
|
||||||
|c: &char| {
|
|c: &char| {
|
||||||
|
@ -76,7 +79,7 @@ async fn main() {
|
||||||
)
|
)
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
/*
|
/*
|
||||||
ctx.write().unwrap().add_morphism(
|
ctx.write().unwrap().add_morphism(
|
||||||
MorphismType{
|
MorphismType{
|
||||||
|
|
Loading…
Reference in a new issue