From 6b2f8ee66f493a8501f255fb8420d4f279c589eb Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 12 Nov 2023 18:07:20 +0100 Subject: [PATCH] use lib-laddertypes & remove old laddertypes implementation --- nested/Cargo.toml | 1 + nested/src/editors/char/mod.rs | 7 +- nested/src/editors/integer/ctx.rs | 3 +- nested/src/editors/integer/editor.rs | 9 +- nested/src/editors/list/cmd.rs | 2 +- nested/src/editors/list/ctx.rs | 3 +- nested/src/editors/list/editor.rs | 9 +- nested/src/editors/list/pty_editor.rs | 10 +- nested/src/editors/product/editor.rs | 5 +- nested/src/editors/product/segment.rs | 3 +- nested/src/editors/sum/editor.rs | 3 +- nested/src/editors/typeterm/cmd.rs | 8 +- nested/src/editors/typeterm/ctx.rs | 3 +- nested/src/editors/typeterm/mod.rs | 47 ++-- nested/src/tree/nav.rs | 4 +- nested/src/tree/node.rs | 9 +- nested/src/tree/treetype.rs | 2 +- nested/src/type_system/context.rs | 23 +- nested/src/type_system/dict.rs | 73 ------ nested/src/type_system/ladder.rs | 71 ----- nested/src/type_system/mod.rs | 11 +- nested/src/type_system/repr_tree.rs | 5 +- nested/src/type_system/term.rs | 361 -------------------------- 23 files changed, 86 insertions(+), 586 deletions(-) delete mode 100644 nested/src/type_system/dict.rs delete mode 100644 nested/src/type_system/ladder.rs delete mode 100644 nested/src/type_system/term.rs diff --git a/nested/Cargo.toml b/nested/Cargo.toml index 7a4c7d0..8814165 100644 --- a/nested/Cargo.toml +++ b/nested/Cargo.toml @@ -7,6 +7,7 @@ version = "0.1.0" [dependencies] #r3vi = { git = "https://git.exobiont.de/senvas/lib-r3vi.git" } r3vi = { path = "../../lib-r3vi" } +laddertypes = { path = "../../lib-laddertypes" } no_deadlocks = "*" cgmath = { version = "0.18.0", features = ["serde"] } termion = "2.0.1" diff --git a/nested/src/editors/char/mod.rs b/nested/src/editors/char/mod.rs index 63b0c00..2521cb1 100644 --- a/nested/src/editors/char/mod.rs +++ b/nested/src/editors/char/mod.rs @@ -6,8 +6,9 @@ use { }, buffer::singleton::* }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, ReprTree, TypeTerm}, + type_system::{Context, ReprTree}, terminal::{TerminalAtom}, tree::{NestedNode, TreeNavResult}, commander::{ObjCommander} @@ -34,7 +35,7 @@ impl ObjCommander for CharEditor { let cmd_obj = cmd_obj.read().unwrap(); let cmd_type = cmd_obj.get_type().clone(); - if cmd_type == (&self.ctx, "( Char )").into() { + if cmd_type == Context::parse(&self.ctx, "Char") { if let Some(cmd_view) = cmd_obj.get_view::>() { let value = cmd_view.get(); @@ -77,7 +78,7 @@ impl CharEditor { NestedNode::new( ctx0.clone(), ReprTree::new_leaf( - ctx0.read().unwrap().type_term_from_str("( Char )").unwrap(), + ctx0.read().unwrap().type_term_from_str("Char").unwrap(), data.get_port().into() ), depth diff --git a/nested/src/editors/integer/ctx.rs b/nested/src/editors/integer/ctx.rs index e9189c9..99c9aa7 100644 --- a/nested/src/editors/integer/ctx.rs +++ b/nested/src/editors/integer/ctx.rs @@ -3,8 +3,9 @@ use { r3vi::{ view::{OuterViewPort, singleton::*} }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm}, + type_system::{Context}, editors::{ list::*, integer::* diff --git a/nested/src/editors/integer/editor.rs b/nested/src/editors/integer/editor.rs index 8c6c393..3e11b34 100644 --- a/nested/src/editors/integer/editor.rs +++ b/nested/src/editors/integer/editor.rs @@ -10,8 +10,9 @@ use { index_hashmap::* } }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm, ReprTree}, + type_system::{Context, ReprTree}, editors::list::{ListCmd, PTYListController, PTYListStyle}, terminal::{ TerminalAtom, TerminalStyle, make_label @@ -40,7 +41,7 @@ impl ObjCommander for DigitEditor { let cmd_obj = cmd_obj.read().unwrap(); let cmd_type = cmd_obj.get_type().clone(); - if cmd_type == (&self.ctx, "( Char )").into() { + if cmd_type == Context::parse(&self.ctx, "Char") { if let Some(cmd_view) = cmd_obj.get_view::>() { let c = cmd_view.get(); @@ -125,7 +126,7 @@ impl DigitEditor { pub fn get_data(&self) -> Arc> { ReprTree::ascend( &ReprTree::new_leaf( - self.ctx.read().unwrap().type_term_from_str("( Seq u32 )").unwrap(), + self.ctx.read().unwrap().type_term_from_str("").unwrap(), self.get_data_port().into() ), self.get_type() @@ -145,7 +146,7 @@ impl PosIntEditor { pub fn new(ctx: Arc>, radix: u32) -> Self { let mut node = Context::make_node( &ctx, - (&ctx, format!("( List ( Digit {} ) )", radix).as_str()).into(), + Context::parse(&ctx, format!(">", radix).as_str()), r3vi::buffer::singleton::SingletonBuffer::new(0).get_port() ).unwrap(); diff --git a/nested/src/editors/list/cmd.rs b/nested/src/editors/list/cmd.rs index d991d5d..74c7fee 100644 --- a/nested/src/editors/list/cmd.rs +++ b/nested/src/editors/list/cmd.rs @@ -26,7 +26,7 @@ impl ListCmd { pub fn into_repr_tree(self, ctx: &Arc>) -> Arc> { let buf = r3vi::buffer::singleton::SingletonBuffer::new(self); ReprTree::new_leaf( - (ctx, "( ListCmd )"), + Context::parse(ctx, "ListCmd"), buf.get_port().into() ) } diff --git a/nested/src/editors/list/ctx.rs b/nested/src/editors/list/ctx.rs index 586db0b..91474f0 100644 --- a/nested/src/editors/list/ctx.rs +++ b/nested/src/editors/list/ctx.rs @@ -1,7 +1,8 @@ use { r3vi::{view::{OuterViewPort, singleton::*}}, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm}, + type_system::{Context}, editors::list::{ListEditor, PTYListController, PTYListStyle} }, std::sync::{Arc, RwLock} diff --git a/nested/src/editors/list/editor.rs b/nested/src/editors/list/editor.rs index 0ba346b..31c1f1b 100644 --- a/nested/src/editors/list/editor.rs +++ b/nested/src/editors/list/editor.rs @@ -3,8 +3,9 @@ use { view::{ViewPort, OuterViewPort, singleton::*, sequence::*}, buffer::{singleton::*, vec::*} }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm, ReprTree}, + type_system::{Context, ReprTree}, editors::list::{ListCursor, ListCursorMode, ListCmd}, tree::{NestedNode, TreeNav, TreeCursor}, diagnostics::Diagnostics, @@ -325,7 +326,7 @@ impl ListEditor { tail_node .send_cmd_obj( ReprTree::new_leaf( - (&self.ctx, "( NestedNode )"), + Context::parse(&self.ctx, "NestedNode"), SingletonBuffer::::new( node.read().unwrap().clone() ).get_port().into() @@ -379,7 +380,7 @@ impl ListEditor { for x in data.iter() { pxv_editor.send_cmd_obj( ReprTree::new_leaf( - (&self.ctx, "( NestedNode )"), + Context::parse(&self.ctx, "NestedNode"), SingletonBuffer::::new( x.read().unwrap().clone() ).get_port().into() @@ -438,7 +439,7 @@ impl ListEditor { for x in data.iter() { cur_editor.send_cmd_obj( ReprTree::new_leaf( - (&self.ctx, "( NestedNode )"), + Context::parse(&self.ctx, "NestedNode"), SingletonBuffer::::new( x.read().unwrap().clone() ).get_port().into() diff --git a/nested/src/editors/list/pty_editor.rs b/nested/src/editors/list/pty_editor.rs index c85b9aa..829aef4 100644 --- a/nested/src/editors/list/pty_editor.rs +++ b/nested/src/editors/list/pty_editor.rs @@ -189,12 +189,12 @@ impl PTYListController { let res = item.write().unwrap().send_cmd_obj(cmd_obj.clone()); let child_close_char = item.read().unwrap().close_char.get(); - match res { + match res { TreeNavResult::Continue => TreeNavResult::Continue, TreeNavResult::Exit => { // child editor returned control, probably for meta-char handling.. - if cmd_obj.read().unwrap().get_type().clone() == ctx.type_term_from_str("( Char )").unwrap() { + if cmd_obj.read().unwrap().get_type().clone() == ctx.type_term_from_str("Char").unwrap() { let co = cmd_obj.read().unwrap(); if let Some(cmd_view) = co.get_view::>() { drop(co); @@ -225,13 +225,13 @@ impl ObjCommander for PTYListController { let mut e = self.editor.write().unwrap(); let cmd_type = cmd_obj.read().unwrap().get_type().clone(); - if cmd_type == (&e.ctx, "( ListCmd )").into() - || cmd_type == (&e.ctx, "( NestedNode )").into() + if cmd_type == Context::parse(&e.ctx, "ListCmd").into() + || cmd_type == Context::parse(&e.ctx, "NestedNode").into() { e.send_cmd_obj( cmd_obj ) } - else if cmd_type == (&e.ctx, "( TerminalEvent )").into() { + else if cmd_type == Context::parse(&e.ctx, "TerminalEvent").into() { let co = cmd_obj.read().unwrap(); if let Some(view) = co.get_view::>() { drop( co ); diff --git a/nested/src/editors/product/editor.rs b/nested/src/editors/product/editor.rs index 97967d1..d3bdd9a 100644 --- a/nested/src/editors/product/editor.rs +++ b/nested/src/editors/product/editor.rs @@ -9,8 +9,9 @@ use { index_hashmap::* } }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm}, + type_system::{Context}, terminal::{ TerminalEditor, TerminalEditorResult, TerminalEvent, TerminalView @@ -202,7 +203,7 @@ impl ObjCommander for ProductEditor { fn send_cmd_obj(&mut self, cmd_obj: Arc>) -> TreeNavResult { let co = cmd_obj.read().unwrap(); let cmd_type = co.get_type().clone(); - let term_event_type = (&self.ctx, "( TerminalEvent )").into(); + let term_event_type = Context::parse(&self.ctx, "TerminalEvent").into(); if cmd_type == term_event_type { if let Some(te_view) = co.get_view::>() { diff --git a/nested/src/editors/product/segment.rs b/nested/src/editors/product/segment.rs index 0e20cb9..0b223f5 100644 --- a/nested/src/editors/product/segment.rs +++ b/nested/src/editors/product/segment.rs @@ -4,8 +4,9 @@ use { OuterViewPort } }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm}, + type_system::{Context}, terminal::{ TerminalStyle, TerminalView, make_label diff --git a/nested/src/editors/sum/editor.rs b/nested/src/editors/sum/editor.rs index dc0c81e..14b7798 100644 --- a/nested/src/editors/sum/editor.rs +++ b/nested/src/editors/sum/editor.rs @@ -6,10 +6,11 @@ use { sequence::*, } }, + laddertypes::{TypeTerm}, crate::{ terminal::TerminalView, editors::list::ListCursorMode, - type_system::{Context, TypeTerm, ReprTree}, + type_system::{Context, ReprTree}, tree::{TreeNav, TreeCursor, TreeNavResult}, diagnostics::{Diagnostics, Message}, tree::NestedNode, diff --git a/nested/src/editors/typeterm/cmd.rs b/nested/src/editors/typeterm/cmd.rs index 57ad081..e219cc8 100644 --- a/nested/src/editors/typeterm/cmd.rs +++ b/nested/src/editors/typeterm/cmd.rs @@ -3,7 +3,7 @@ use { view::{singleton::*} }, crate::{ - type_system::{ReprTree}, + type_system::{Context, ReprTree}, editors::{list::{ListEditor, ListCmd, ListCursorMode}}, tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor}, commander::ObjCommander @@ -20,7 +20,7 @@ impl ObjCommander for TypeTermEditor { let cmd_obj = co.clone(); let cmd_obj = cmd_obj.read().unwrap(); - if cmd_obj.get_type().clone() == (&self.ctx, "( Char )").into() { + if cmd_obj.get_type().clone() == Context::parse(&self.ctx, "Char") { if let Some(cmd_view) = cmd_obj.get_view::>() { let c = cmd_view.get(); @@ -231,11 +231,11 @@ impl ObjCommander for TypeTermEditor { match &self.state { State::Any => { let cmd_repr = co.read().unwrap(); - if cmd_repr.get_type().clone() == (&self.ctx, "( NestedNode )").into() { + if cmd_repr.get_type().clone() == Context::parse(&self.ctx, "NestedNode") { if let Some(view) = cmd_repr.get_view::>() { let node = view.get(); - if node.data.read().unwrap().get_type().clone() == (&self.ctx, "( Char )").into() { + if node.data.read().unwrap().get_type().clone() == Context::parse(&self.ctx, "Char") { self.set_state( State::AnySymbol ); } else { self.set_state( State::Ladder ); diff --git a/nested/src/editors/typeterm/ctx.rs b/nested/src/editors/typeterm/ctx.rs index 6ba6b47..4ad5b55 100644 --- a/nested/src/editors/typeterm/ctx.rs +++ b/nested/src/editors/typeterm/ctx.rs @@ -2,8 +2,9 @@ use { r3vi::{ view::{OuterViewPort, singleton::*} }, + laddertypes::{TypeTerm}, crate::{ - type_system::{Context, TypeTerm, MorphismTypePattern}, + type_system::{Context, MorphismTypePattern}, terminal::{TerminalStyle, TerminalProjections}, editors::{ list::{PTYListStyle, PTYListController, ListEditor, ListSegmentSequence}, diff --git a/nested/src/editors/typeterm/mod.rs b/nested/src/editors/typeterm/mod.rs index b53b0a8..d15cbb4 100644 --- a/nested/src/editors/typeterm/mod.rs +++ b/nested/src/editors/typeterm/mod.rs @@ -9,8 +9,9 @@ use { view::{OuterViewPort, singleton::*}, buffer::{singleton::*} }, + laddertypes::{TypeID, TypeTerm}, crate::{ - type_system::{Context, TypeID, TypeTerm, ReprTree}, + type_system::{Context, ReprTree}, editors::{list::{ListCursorMode, ListEditor, ListCmd}}, tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor}, commander::ObjCommander @@ -80,7 +81,7 @@ impl TypeTermEditor { node.send_cmd_obj( ReprTree::new_leaf( - (&ctx, "( NestedNode )"), + Context::parse(&ctx, "NestedNode"), SingletonBuffer::new(arg_node).get_port().into() ) ); @@ -98,7 +99,7 @@ impl TypeTermEditor { node.send_cmd_obj( ReprTree::new_leaf( - (&ctx, "( NestedNode )"), + Context::parse(&ctx, "NestedNode"), SingletonBuffer::new(arg_node).get_port().into() ) ); @@ -132,37 +133,37 @@ impl TypeTermEditor { fn set_state(&mut self, new_state: State) { let mut node = match new_state { State::Any => { - Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::Sym )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, ""), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::Sym") ) } State::App => { - Context::make_node( &self.ctx, (&self.ctx, "( List Type )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::App )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, ""), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::App") ) } State::Ladder => { - Context::make_node( &self.ctx, (&self.ctx, "( List Type )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::Ladder )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, ""), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::Ladder") ) } State::AnySymbol => { - Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::Sym )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, ""), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::Sym") ) }, State::FunSymbol => { - Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::Sym::Fun )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, ""), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::Sym::Fun") ) }, State::VarSymbol => { - Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::Sym::Var )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, ""), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::Sym::Var") ) } State::Num => { crate::editors::integer::PosIntEditor::new(self.ctx.clone(), 10) .into_node() - .morph( (&self.ctx, "( Type::Lit::Num )").into() ) + .morph( Context::parse(&self.ctx, "Type::Lit::Num") ) } State::Char => { - Context::make_node( &self.ctx, (&self.ctx, "( Char )").into(), self.depth.map(|x| x) ).unwrap() - .morph( (&self.ctx, "( Type::Lit::Char )").into() ) + Context::make_node( &self.ctx, Context::parse(&self.ctx, "Char"), self.depth.map(|x| x) ).unwrap() + .morph( Context::parse(&self.ctx, "Type::Lit::Char") ) } }; @@ -179,8 +180,8 @@ impl TypeTermEditor { ctx.write().unwrap().meta_chars.push('~'); ctx.write().unwrap().meta_chars.push('<'); - let mut symb_node = Context::make_node( &ctx, (&ctx, "( List Char )").into(), depth ).unwrap(); - symb_node = symb_node.morph( (&ctx, "( Type::Sym )").into() ); + let mut symb_node = Context::make_node( &ctx, Context::parse(&ctx, ""), depth ).unwrap(); + symb_node = symb_node.morph( Context::parse(&ctx, "Type::Sym") ); Self::with_node( ctx.clone(), @@ -193,7 +194,7 @@ impl TypeTermEditor { let buf = SingletonBuffer::::new( TypeTerm::unit() ); let data = Arc::new(RwLock::new(ReprTree::new( - (&ctx, "( Type )") + Context::parse(&ctx, "Type") ))); let editor = TypeTermEditor { @@ -307,7 +308,7 @@ impl TypeTermEditor { if subladder_list_edit.data.len() == 1 { let it_node = subladder_list_edit.data.get(0); let it_node = it_node.read().unwrap(); - if it_node.get_type() == (&self.ctx, "( Type )").into() { + if it_node.get_type() == Context::parse(&self.ctx, "Type") { let other_tt = it_node.get_edit::().unwrap(); let mut other_tt = other_tt.write().unwrap(); @@ -384,7 +385,7 @@ impl TypeTermEditor { self.goto(TreeCursor::home()); self.send_child_cmd( ReprTree::new_leaf( - (&self.ctx, "( NestedNode )"), + Context::parse(&self.ctx, "NestedNode"), SingletonBuffer::new( old_edit_node ).get_port().into() ) ); diff --git a/nested/src/tree/nav.rs b/nested/src/tree/nav.rs index 67acee3..9d85cdd 100644 --- a/nested/src/tree/nav.rs +++ b/nested/src/tree/nav.rs @@ -21,10 +21,10 @@ use { cgmath::Vector2, }; -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Copy, Eq, PartialEq, Debug)] pub enum TreeNavResult { Continue, Exit } -#[derive(Clone, Copy, Eq, PartialEq)] +#[derive(Clone, Copy, Eq, PartialEq, Debug)] pub enum TreeHeightOp { P, Q, Max } pub trait TreeNav { diff --git a/nested/src/tree/node.rs b/nested/src/tree/node.rs index 75fdf3e..1406c96 100644 --- a/nested/src/tree/node.rs +++ b/nested/src/tree/node.rs @@ -5,8 +5,9 @@ use { view::{View, ViewPort, OuterViewPort, AnyOuterViewPort, singleton::*, sequence::*}, buffer::{singleton::*} }, + laddertypes::{TypeTerm}, crate::{ - type_system::{ReprTree, Context, TypeTerm}, + type_system::{ReprTree, Context}, terminal::{TerminalView, TerminalEvent, TerminalEditor, TerminalEditorResult, TerminalAtom}, diagnostics::{Diagnostics, Message}, tree::{TreeNav, TreeCursor, TreeNavResult, TreeHeightOp}, @@ -124,7 +125,7 @@ impl NestedNode { NestedNode::new( ctx.clone(), ReprTree::new_leaf( - (&ctx, "( Char )"), + Context::parse(&ctx, "Char"), buf.get_port().into() ), SingletonBuffer::new(0).get_port() @@ -194,7 +195,7 @@ impl NestedNode { pub fn get_data_port<'a, V: View + ?Sized + 'static>(&'a self, type_str: impl Iterator) -> Option> where V::Msg: Clone { let ctx = self.ctx.clone(); - let type_ladder = type_str.map(|s| ((&ctx, s)).into()); + let type_ladder = type_str.map(|s| Context::parse(&ctx, s)); let repr_tree = ReprTree::descend_ladder(&self.data, type_ladder)?; repr_tree.clone().read().unwrap() @@ -256,7 +257,7 @@ impl TerminalEditor for NestedNode { if let Some(cmd) = self.cmd.get() { cmd.write().unwrap().send_cmd_obj( ReprTree::new_leaf( - self.ctx.read().unwrap().type_term_from_str("( TerminalEvent )").unwrap(), + self.ctx.read().unwrap().type_term_from_str("TerminalEvent").unwrap(), AnyOuterViewPort::from(buf.get_port()) )); } diff --git a/nested/src/tree/treetype.rs b/nested/src/tree/treetype.rs index 07f0dce..9f66849 100644 --- a/nested/src/tree/treetype.rs +++ b/nested/src/tree/treetype.rs @@ -1,7 +1,7 @@ use { + laddertypes::{TypeTerm, TypeID}, crate::{ - type_system::{TypeTerm, TypeID}, tree::{TreeAddr} } }; diff --git a/nested/src/type_system/context.rs b/nested/src/type_system/context.rs index 41df4a5..bf4f8c4 100644 --- a/nested/src/type_system/context.rs +++ b/nested/src/type_system/context.rs @@ -1,7 +1,8 @@ use { r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}}, + laddertypes::{TypeDict, TypeTerm, TypeID}, crate::{ - type_system::{TypeDict, TypeTerm, TypeID, ReprTree}, + type_system::{ReprTree}, tree::NestedNode }, std::{ @@ -135,12 +136,6 @@ impl Default for Context { } } -impl Into for (&Arc>, &str) { - fn into(self) -> TypeTerm { - self.0.read().unwrap().type_term_from_str(self.1).expect("could not parse type term") - } -} - impl Context { pub fn with_parent(parent: Option>>) -> Self { Context { @@ -174,6 +169,10 @@ impl Context { } } + pub fn parse(ctx: &Arc>, s: &str) -> TypeTerm { + ctx.read().unwrap().type_term_from_str(s).expect("could not parse type term") + } + pub fn add_typename(&mut self, tn: &str) -> TypeID { self.type_dict.write().unwrap().add_typename(tn.to_string()) } @@ -234,12 +233,12 @@ impl Context { } } - pub fn type_term_from_str(&self, tn: &str) -> Option { - self.type_dict.read().unwrap().type_term_from_str(&tn) + pub fn type_term_from_str(&self, tn: &str) -> Result { + self.type_dict.write().unwrap().parse(&tn) } pub fn type_term_to_str(&self, t: &TypeTerm) -> String { - self.type_dict.read().unwrap().type_term_to_str(&t) + self.type_dict.read().unwrap().unparse(&t) } pub fn add_node_ctor(&mut self, tn: &str, mk_editor: Arc>, TypeTerm, OuterViewPort>) -> Option + Send + Sync>) { @@ -332,8 +331,8 @@ impl Context { /// adds an object without any representations pub fn add_obj(ctx: Arc>, name: String, typename: &str) { let type_tag = ctx.read().unwrap() - .type_dict.read().unwrap() - .type_term_from_str(typename).unwrap(); + .type_dict.write().unwrap() + .parse(typename).unwrap(); if let Some(node) = Context::make_node(&ctx, type_tag, SingletonBuffer::new(0).get_port()) { ctx.write().unwrap().nodes.insert(name, node); diff --git a/nested/src/type_system/dict.rs b/nested/src/type_system/dict.rs deleted file mode 100644 index b8fd44c..0000000 --- a/nested/src/type_system/dict.rs +++ /dev/null @@ -1,73 +0,0 @@ -use { - crate::{ - utils::Bimap, - type_system::{TypeTerm} - } -}; - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -#[derive(Eq, PartialEq, Hash, Clone, Debug)] -pub enum TypeID { - Fun(u64), - Var(u64) -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -pub struct TypeDict { - typenames: Bimap, - type_lit_counter: u64, - type_var_counter: u64, -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -impl TypeDict { - pub fn new() -> Self { - TypeDict { - typenames: Bimap::new(), - type_lit_counter: 0, - type_var_counter: 0, - } - } - - pub fn add_varname(&mut self, tn: String) -> TypeID { - let tyid = TypeID::Var(self.type_var_counter); - self.type_var_counter += 1; - self.typenames.insert(tn, tyid.clone()); - tyid - } - - pub fn add_typename(&mut self, tn: String) -> TypeID { - let tyid = TypeID::Fun(self.type_lit_counter); - self.type_lit_counter += 1; - self.typenames.insert(tn, tyid.clone()); - tyid - } - - pub fn add_synonym(&mut self, new: String, old: String) { - if let Some(tyid) = self.get_typeid(&old) { - self.typenames.insert(new, tyid); - } - } - - pub fn get_typename(&self, tid: &TypeID) -> Option { - self.typenames.my.get(tid).cloned() - } - - pub fn get_typeid(&self, tn: &String) -> Option { - self.typenames.mλ.get(tn).cloned() - } - - pub fn type_term_from_str(&self, typename: &str) -> Option { - TypeTerm::from_str(typename, &self.typenames.mλ) - } - - pub fn type_term_to_str(&self, term: &TypeTerm) -> String { - term.to_str(&self.typenames.my) - } -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - diff --git a/nested/src/type_system/ladder.rs b/nested/src/type_system/ladder.rs deleted file mode 100644 index ca7fef0..0000000 --- a/nested/src/type_system/ladder.rs +++ /dev/null @@ -1,71 +0,0 @@ -use { - crate::type_system::{TypeTerm, TypeID}, - std::collections::HashMap -}; - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -#[derive(Clone, Eq, PartialEq, Hash, Debug)] -pub struct TypeLadder(pub Vec); - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -impl From> for TypeLadder { - fn from(l: Vec) -> Self { - TypeLadder(l) - } -} - -impl From for TypeLadder { - fn from(l: TypeTerm) -> Self { - TypeLadder(vec![ l ]) - } -} - -impl TypeLadder { - /// if compatible, returns the number of descents neccesary - pub fn is_compatible_with(&self, other: &TypeLadder) -> Option { - if let Some(other_top_type) = other.0.first() { - for (i, t) in self.0.iter().enumerate() { - if t == other_top_type { - return Some(i); - } - } - - None - } else { - None - } - } - - pub fn is_matching_repr(&self, other: &TypeLadder) -> Result> { - if let Some(start) = self.is_compatible_with(other) { - for (i, (t1, t2)) in self.0.iter().skip(start).zip(other.0.iter()).enumerate() { - if t1 != t2 { - return Err(Some((start, i))); - } - } - - Ok(start) - } else { - Err(None) - } - } - - pub fn to_str1(&self, names: &HashMap) -> String { - let mut s = String::new(); - let mut first = true; - - for t in self.0.iter() { - if !first { - s = s + "~"; - } - first = false; - s = s + &t.to_str(names); - } - s - } -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - diff --git a/nested/src/type_system/mod.rs b/nested/src/type_system/mod.rs index f52f6ef..6d52a5b 100644 --- a/nested/src/type_system/mod.rs +++ b/nested/src/type_system/mod.rs @@ -1,15 +1,8 @@ pub mod context; - -pub mod dict; -pub mod term; -//pub mod ladder; pub mod repr_tree; pub use { - dict::*, -// ladder::*, - repr_tree::*, - term::*, - context::{Context, MorphismMode, MorphismType, MorphismTypePattern} + context::{Context, MorphismMode, MorphismType, MorphismTypePattern}, + repr_tree::ReprTree }; diff --git a/nested/src/type_system/repr_tree.rs b/nested/src/type_system/repr_tree.rs index eeeb8cf..611565c 100644 --- a/nested/src/type_system/repr_tree.rs +++ b/nested/src/type_system/repr_tree.rs @@ -1,7 +1,8 @@ use { r3vi::view::{AnyOuterViewPort, OuterViewPort, View}, + laddertypes::{TypeTerm}, crate::{ - type_system::{TypeTerm, Context} + type_system::{Context} }, std::{ collections::HashMap, @@ -50,7 +51,7 @@ impl ReprTree { pub fn from_char(ctx: &Arc>, c: char) -> Arc> { let buf = r3vi::buffer::singleton::SingletonBuffer::::new(c); ReprTree::new_leaf( - (ctx, "( Char )"), + Context::parse(ctx, "Char"), buf.get_port().into() ) } diff --git a/nested/src/type_system/term.rs b/nested/src/type_system/term.rs deleted file mode 100644 index 12c1c15..0000000 --- a/nested/src/type_system/term.rs +++ /dev/null @@ -1,361 +0,0 @@ -use { - crate::{type_system::{TypeID}}, - std::collections::HashMap -}; - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - - -#[derive(Clone, PartialEq, Eq, Hash, Debug)] -pub enum TypeTerm { - - /* Atomic Terms */ - - // Base types from dictionary - TypeID(TypeID), - - // Literals - Num(i64), - Char(char), - - - - /* Complex Terms */ - - // Type Parameters - // avoid currying to save space & indirection - App(Vec< TypeTerm >), - - // Type Ladders - Ladder(Vec< TypeTerm >), -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -impl TypeTerm { - pub fn unit() -> Self { - TypeTerm::Ladder(vec![]) - } - - pub fn new(id: TypeID) -> Self { - TypeTerm::TypeID(id) - } - - pub fn arg(&mut self, t: impl Into) -> &mut Self { - match self { - TypeTerm::App(args) => { - args.push(t.into()); - } - - _ => { - *self = TypeTerm::App(vec![ - self.clone(), - t.into() - ]) - } - } - - self - } - - pub fn num_arg(&mut self, v: i64) -> &mut Self { - self.arg(TypeTerm::Num(v)) - } - - pub fn char_arg(&mut self, c: char) -> &mut Self { - self.arg(TypeTerm::Char(c)) - } - - /// transform term to have at max 2 entries in Application list - pub fn curry(&self) -> Self { - match self { - TypeTerm::App(head) => { - let mut head = head.clone(); - if head.len() > 2 { - let mut tail = head.split_off(2); - - TypeTerm::App(vec![ - TypeTerm::App(head), - if tail.len() > 1 { - TypeTerm::App(tail).curry() - } else { - tail.remove(0) - } - ]) - } else { - TypeTerm::App(head) - } - } - - TypeTerm::Ladder(l) => { - TypeTerm::Ladder( l.iter().map(|x| x.curry()).collect() ) - } - - atom => { atom.clone() } - } - } - - /// summarize all curried applications into one vec - pub fn decurry(&mut self) -> &mut Self { - match self { - TypeTerm::App(args) => { - if args.len() > 0 { - let mut a0 = args.remove(0); - a0.decurry(); - match a0 { - TypeTerm::App(sub_args) => { - for (i,x) in sub_args.into_iter().enumerate() { - args.insert(i, x); - } - } - other => { args.insert(0, other); } - } - } - } - TypeTerm::Ladder(args) => { - for x in args.iter_mut() { - x.decurry(); - } - } - _ => {} - } - - self - } - - /// does the type contain ladders (false) or is it 'flat' (true) ? - pub fn is_flat(&self) -> bool { - match self { - TypeTerm::TypeID(_) => true, - TypeTerm::Num(_) => true, - TypeTerm::Char(_) => true, - TypeTerm::App(args) => args.iter().fold(true, |s,x| s && x.is_flat()), - TypeTerm::Ladder(_) => false - } - } - - pub fn get_lnf_vec(self) -> Vec { - match self.normalize() { - TypeTerm::Ladder( v ) => { - v - }, - _ => { - unreachable!(); - } - } - } - - /// transmute self into Ladder-Normal-Form - /// - /// Example: - /// ~Char> ⇒ >~ - pub fn normalize(self) -> Self { - let mut new_ladder = Vec::::new(); - - match self { - TypeTerm::Ladder(args) => { - for x in args.into_iter() { - new_ladder.push(x.normalize()); - } - } - - TypeTerm::App(args) => { - let mut args_iter = args.into_iter(); - if let Some(head) = args_iter.next() { - - let mut stage1_args = vec![ head.clone() ]; - let mut stage2_args = vec![ head.clone() ]; - - let mut done = false; - - for x in args_iter { - match x.normalize() { - TypeTerm::Ladder(mut ladder) => { - // normalize this ladder - - if !done { - if ladder.len() > 2 { - stage1_args.push( ladder.remove(0) ); - stage2_args.push( TypeTerm::Ladder(ladder.to_vec()) ); - done = true; - } else if ladder.len() == 1 { - stage1_args.push( ladder[0].clone() ); - stage2_args.push( ladder[0].clone() ); - } else { - // empty type ? - } - - } else { - stage1_args.push( TypeTerm::Ladder(ladder.clone()) ); - stage2_args.push( TypeTerm::Ladder(ladder.clone()) ); - } - }, - _ => { - unreachable!("x is in LNF"); - } - } - } - - new_ladder.push(TypeTerm::Ladder(stage1_args)); - new_ladder.push(TypeTerm::Ladder(stage2_args)); - } - } - - atom => { - new_ladder.push(atom); - } - } - - TypeTerm::Ladder( new_ladder ) - } - - pub fn is_semantic_supertype_of(&self, t: &TypeTerm) -> Option<( usize, TypeTerm )> { - t.is_semantic_subtype_of(self) - } - - // returns ladder-step of first match and provided representation-type - pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<( usize, TypeTerm )> { - let provided_lnf = self.clone().get_lnf_vec(); - let expected_lnf = expected_type.clone().get_lnf_vec(); - - for i in 0..provided_lnf.len() { - if provided_lnf[i] == expected_lnf[0] { - return Some((i, TypeTerm::Ladder( - provided_lnf[i..].into_iter().cloned().collect() - ))) - } - } - - None - } - - pub fn is_syntactic_subtype_of(&self, expected_type: &TypeTerm) -> Result> { - if let Some((first_match, provided_type)) = self.is_semantic_subtype_of( expected_type ) { - let provided_lnf = self.clone().get_lnf_vec(); - let expected_lnf = expected_type.clone().get_lnf_vec(); - - let l = usize::min( provided_lnf.len(), expected_lnf.len() ); - - for i in 0..l { - - if provided_lnf[i] != expected_lnf[i] { - return Err(Some((first_match, i))) - } - } - - Ok(l-1) - } else { - Err(None) - } - } - - /* this function is deprecated and only partially working, - wontfix, will be replaced by TypeTerm-Editor - */ - pub fn from_str(s: &str, names: &HashMap) -> Option { - let mut term_stack = Vec::>::new(); - - for token in s.split_whitespace() { - match token { - "(" => { - term_stack.push(None); - } - ")" => { - let t = term_stack.pop().unwrap(); - if term_stack.len() > 0 { - let f = term_stack.last_mut().unwrap(); - if let Some(f) = f { - f.arg(t.unwrap()); - } else { - //error - } - } else { - return t; - } - } - atom => { - if let Some(f) = term_stack.last_mut() { - match f { - Some(f) => { - let mut chars = atom.chars(); - let first = chars.next().unwrap(); - - if first.is_numeric() { - f.num_arg(i64::from_str_radix(atom, 10).unwrap()); - } else if first == '\'' { - if let Some(mut c) = chars.next() { - if c == '\\' { - if let Some('n') = chars.next() { - c = '\n'; - } - } - f.char_arg(c); - } - } else { - f.arg(TypeTerm::new( - names.get(atom) - .expect(&format!("invalid atom {}", atom)).clone() - )); - } - } - None => { - *f = Some(TypeTerm::new( - names.get(atom).expect(&format!("invalid atom {}", atom)).clone(), - )); - } - } - } - } - } - } - - None - } - - pub fn to_str(&self, names: &HashMap) -> String { - match self { - TypeTerm::App(args) => { - let mut out = String::new(); - - out.push_str(&"<"); - - let mut first = true; - for x in args.iter() { - if !first { - out.push_str(&" "); - } else { - first = false; - } - - out.push_str(&x.to_str(names)); - } - - out.push_str(&">"); - - out - } - - TypeTerm::Ladder(l) => { - let mut out = String::new(); - - let mut first = true; - for x in l.iter() { - if !first { - out.push_str(&"~"); - } else { - first = false; - } - - out.push_str(&x.to_str(names)); - } - - out - } - - TypeTerm::Num(n) => format!("{}", n), - TypeTerm::Char('\n') => format!("'\\n'"), - TypeTerm::Char(c) => format!("'{}'", c), - TypeTerm::TypeID(id) => format!("{}", names[id]), - } - } -}