use lib-laddertypes & remove old laddertypes implementation
This commit is contained in:
parent
5aac404bf2
commit
6b2f8ee66f
23 changed files with 86 additions and 586 deletions
|
@ -7,6 +7,7 @@ version = "0.1.0"
|
||||||
[dependencies]
|
[dependencies]
|
||||||
#r3vi = { git = "https://git.exobiont.de/senvas/lib-r3vi.git" }
|
#r3vi = { git = "https://git.exobiont.de/senvas/lib-r3vi.git" }
|
||||||
r3vi = { path = "../../lib-r3vi" }
|
r3vi = { path = "../../lib-r3vi" }
|
||||||
|
laddertypes = { path = "../../lib-laddertypes" }
|
||||||
no_deadlocks = "*"
|
no_deadlocks = "*"
|
||||||
cgmath = { version = "0.18.0", features = ["serde"] }
|
cgmath = { version = "0.18.0", features = ["serde"] }
|
||||||
termion = "2.0.1"
|
termion = "2.0.1"
|
||||||
|
|
|
@ -6,8 +6,9 @@ use {
|
||||||
},
|
},
|
||||||
buffer::singleton::*
|
buffer::singleton::*
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, ReprTree, TypeTerm},
|
type_system::{Context, ReprTree},
|
||||||
terminal::{TerminalAtom},
|
terminal::{TerminalAtom},
|
||||||
tree::{NestedNode, TreeNavResult},
|
tree::{NestedNode, TreeNavResult},
|
||||||
commander::{ObjCommander}
|
commander::{ObjCommander}
|
||||||
|
@ -34,7 +35,7 @@ impl ObjCommander for CharEditor {
|
||||||
let cmd_obj = cmd_obj.read().unwrap();
|
let cmd_obj = cmd_obj.read().unwrap();
|
||||||
let cmd_type = cmd_obj.get_type().clone();
|
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::<dyn SingletonView<Item = char>>() {
|
if let Some(cmd_view) = cmd_obj.get_view::<dyn SingletonView<Item = char>>() {
|
||||||
let value = cmd_view.get();
|
let value = cmd_view.get();
|
||||||
|
|
||||||
|
@ -77,7 +78,7 @@ impl CharEditor {
|
||||||
NestedNode::new(
|
NestedNode::new(
|
||||||
ctx0.clone(),
|
ctx0.clone(),
|
||||||
ReprTree::new_leaf(
|
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()
|
data.get_port().into()
|
||||||
),
|
),
|
||||||
depth
|
depth
|
||||||
|
|
|
@ -3,8 +3,9 @@ use {
|
||||||
r3vi::{
|
r3vi::{
|
||||||
view::{OuterViewPort, singleton::*}
|
view::{OuterViewPort, singleton::*}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm},
|
type_system::{Context},
|
||||||
editors::{
|
editors::{
|
||||||
list::*,
|
list::*,
|
||||||
integer::*
|
integer::*
|
||||||
|
|
|
@ -10,8 +10,9 @@ use {
|
||||||
index_hashmap::*
|
index_hashmap::*
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm, ReprTree},
|
type_system::{Context, ReprTree},
|
||||||
editors::list::{ListCmd, PTYListController, PTYListStyle},
|
editors::list::{ListCmd, PTYListController, PTYListStyle},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalAtom, TerminalStyle, make_label
|
TerminalAtom, TerminalStyle, make_label
|
||||||
|
@ -40,7 +41,7 @@ impl ObjCommander for DigitEditor {
|
||||||
let cmd_obj = cmd_obj.read().unwrap();
|
let cmd_obj = cmd_obj.read().unwrap();
|
||||||
let cmd_type = cmd_obj.get_type().clone();
|
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::<dyn SingletonView<Item = char>>() {
|
if let Some(cmd_view) = cmd_obj.get_view::<dyn SingletonView<Item = char>>() {
|
||||||
let c = cmd_view.get();
|
let c = cmd_view.get();
|
||||||
|
|
||||||
|
@ -125,7 +126,7 @@ impl DigitEditor {
|
||||||
pub fn get_data(&self) -> Arc<RwLock<ReprTree>> {
|
pub fn get_data(&self) -> Arc<RwLock<ReprTree>> {
|
||||||
ReprTree::ascend(
|
ReprTree::ascend(
|
||||||
&ReprTree::new_leaf(
|
&ReprTree::new_leaf(
|
||||||
self.ctx.read().unwrap().type_term_from_str("( Seq u32 )").unwrap(),
|
self.ctx.read().unwrap().type_term_from_str("<Seq u32>").unwrap(),
|
||||||
self.get_data_port().into()
|
self.get_data_port().into()
|
||||||
),
|
),
|
||||||
self.get_type()
|
self.get_type()
|
||||||
|
@ -145,7 +146,7 @@ impl PosIntEditor {
|
||||||
pub fn new(ctx: Arc<RwLock<Context>>, radix: u32) -> Self {
|
pub fn new(ctx: Arc<RwLock<Context>>, radix: u32) -> Self {
|
||||||
let mut node = Context::make_node(
|
let mut node = Context::make_node(
|
||||||
&ctx,
|
&ctx,
|
||||||
(&ctx, format!("( List ( Digit {} ) )", radix).as_str()).into(),
|
Context::parse(&ctx, format!("<List <Digit {}>>", radix).as_str()),
|
||||||
r3vi::buffer::singleton::SingletonBuffer::new(0).get_port()
|
r3vi::buffer::singleton::SingletonBuffer::new(0).get_port()
|
||||||
).unwrap();
|
).unwrap();
|
||||||
|
|
||||||
|
|
|
@ -26,7 +26,7 @@ impl ListCmd {
|
||||||
pub fn into_repr_tree(self, ctx: &Arc<RwLock<Context>>) -> Arc<RwLock<ReprTree>> {
|
pub fn into_repr_tree(self, ctx: &Arc<RwLock<Context>>) -> Arc<RwLock<ReprTree>> {
|
||||||
let buf = r3vi::buffer::singleton::SingletonBuffer::new(self);
|
let buf = r3vi::buffer::singleton::SingletonBuffer::new(self);
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(ctx, "( ListCmd )"),
|
Context::parse(ctx, "ListCmd"),
|
||||||
buf.get_port().into()
|
buf.get_port().into()
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,7 +1,8 @@
|
||||||
use {
|
use {
|
||||||
r3vi::{view::{OuterViewPort, singleton::*}},
|
r3vi::{view::{OuterViewPort, singleton::*}},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm},
|
type_system::{Context},
|
||||||
editors::list::{ListEditor, PTYListController, PTYListStyle}
|
editors::list::{ListEditor, PTYListController, PTYListStyle}
|
||||||
},
|
},
|
||||||
std::sync::{Arc, RwLock}
|
std::sync::{Arc, RwLock}
|
||||||
|
|
|
@ -3,8 +3,9 @@ use {
|
||||||
view::{ViewPort, OuterViewPort, singleton::*, sequence::*},
|
view::{ViewPort, OuterViewPort, singleton::*, sequence::*},
|
||||||
buffer::{singleton::*, vec::*}
|
buffer::{singleton::*, vec::*}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm, ReprTree},
|
type_system::{Context, ReprTree},
|
||||||
editors::list::{ListCursor, ListCursorMode, ListCmd},
|
editors::list::{ListCursor, ListCursorMode, ListCmd},
|
||||||
tree::{NestedNode, TreeNav, TreeCursor},
|
tree::{NestedNode, TreeNav, TreeCursor},
|
||||||
diagnostics::Diagnostics,
|
diagnostics::Diagnostics,
|
||||||
|
@ -325,7 +326,7 @@ impl ListEditor {
|
||||||
tail_node
|
tail_node
|
||||||
.send_cmd_obj(
|
.send_cmd_obj(
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&self.ctx, "( NestedNode )"),
|
Context::parse(&self.ctx, "NestedNode"),
|
||||||
SingletonBuffer::<NestedNode>::new(
|
SingletonBuffer::<NestedNode>::new(
|
||||||
node.read().unwrap().clone()
|
node.read().unwrap().clone()
|
||||||
).get_port().into()
|
).get_port().into()
|
||||||
|
@ -379,7 +380,7 @@ impl ListEditor {
|
||||||
for x in data.iter() {
|
for x in data.iter() {
|
||||||
pxv_editor.send_cmd_obj(
|
pxv_editor.send_cmd_obj(
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&self.ctx, "( NestedNode )"),
|
Context::parse(&self.ctx, "NestedNode"),
|
||||||
SingletonBuffer::<NestedNode>::new(
|
SingletonBuffer::<NestedNode>::new(
|
||||||
x.read().unwrap().clone()
|
x.read().unwrap().clone()
|
||||||
).get_port().into()
|
).get_port().into()
|
||||||
|
@ -438,7 +439,7 @@ impl ListEditor {
|
||||||
for x in data.iter() {
|
for x in data.iter() {
|
||||||
cur_editor.send_cmd_obj(
|
cur_editor.send_cmd_obj(
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&self.ctx, "( NestedNode )"),
|
Context::parse(&self.ctx, "NestedNode"),
|
||||||
SingletonBuffer::<NestedNode>::new(
|
SingletonBuffer::<NestedNode>::new(
|
||||||
x.read().unwrap().clone()
|
x.read().unwrap().clone()
|
||||||
).get_port().into()
|
).get_port().into()
|
||||||
|
|
|
@ -189,12 +189,12 @@ impl PTYListController {
|
||||||
let res = item.write().unwrap().send_cmd_obj(cmd_obj.clone());
|
let res = item.write().unwrap().send_cmd_obj(cmd_obj.clone());
|
||||||
let child_close_char = item.read().unwrap().close_char.get();
|
let child_close_char = item.read().unwrap().close_char.get();
|
||||||
|
|
||||||
match res {
|
match res {
|
||||||
TreeNavResult::Continue => TreeNavResult::Continue,
|
TreeNavResult::Continue => TreeNavResult::Continue,
|
||||||
TreeNavResult::Exit => {
|
TreeNavResult::Exit => {
|
||||||
// child editor returned control, probably for meta-char handling..
|
// 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();
|
let co = cmd_obj.read().unwrap();
|
||||||
if let Some(cmd_view) = co.get_view::<dyn SingletonView<Item = char>>() {
|
if let Some(cmd_view) = co.get_view::<dyn SingletonView<Item = char>>() {
|
||||||
drop(co);
|
drop(co);
|
||||||
|
@ -225,13 +225,13 @@ impl ObjCommander for PTYListController {
|
||||||
let mut e = self.editor.write().unwrap();
|
let mut e = self.editor.write().unwrap();
|
||||||
let cmd_type = cmd_obj.read().unwrap().get_type().clone();
|
let cmd_type = cmd_obj.read().unwrap().get_type().clone();
|
||||||
|
|
||||||
if cmd_type == (&e.ctx, "( ListCmd )").into()
|
if cmd_type == Context::parse(&e.ctx, "ListCmd").into()
|
||||||
|| cmd_type == (&e.ctx, "( NestedNode )").into()
|
|| cmd_type == Context::parse(&e.ctx, "NestedNode").into()
|
||||||
{
|
{
|
||||||
e.send_cmd_obj( cmd_obj )
|
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();
|
let co = cmd_obj.read().unwrap();
|
||||||
if let Some(view) = co.get_view::<dyn SingletonView<Item = TerminalEvent>>() {
|
if let Some(view) = co.get_view::<dyn SingletonView<Item = TerminalEvent>>() {
|
||||||
drop( co );
|
drop( co );
|
||||||
|
|
|
@ -9,8 +9,9 @@ use {
|
||||||
index_hashmap::*
|
index_hashmap::*
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm},
|
type_system::{Context},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalEditor, TerminalEditorResult,
|
TerminalEditor, TerminalEditorResult,
|
||||||
TerminalEvent, TerminalView
|
TerminalEvent, TerminalView
|
||||||
|
@ -202,7 +203,7 @@ impl ObjCommander for ProductEditor {
|
||||||
fn send_cmd_obj(&mut self, cmd_obj: Arc<RwLock<ReprTree>>) -> TreeNavResult {
|
fn send_cmd_obj(&mut self, cmd_obj: Arc<RwLock<ReprTree>>) -> TreeNavResult {
|
||||||
let co = cmd_obj.read().unwrap();
|
let co = cmd_obj.read().unwrap();
|
||||||
let cmd_type = co.get_type().clone();
|
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 cmd_type == term_event_type {
|
||||||
if let Some(te_view) = co.get_view::<dyn SingletonView<Item = TerminalEvent>>() {
|
if let Some(te_view) = co.get_view::<dyn SingletonView<Item = TerminalEvent>>() {
|
||||||
|
|
|
@ -4,8 +4,9 @@ use {
|
||||||
OuterViewPort
|
OuterViewPort
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm},
|
type_system::{Context},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalStyle, TerminalView,
|
TerminalStyle, TerminalView,
|
||||||
make_label
|
make_label
|
||||||
|
|
|
@ -6,10 +6,11 @@ use {
|
||||||
sequence::*,
|
sequence::*,
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
terminal::TerminalView,
|
terminal::TerminalView,
|
||||||
editors::list::ListCursorMode,
|
editors::list::ListCursorMode,
|
||||||
type_system::{Context, TypeTerm, ReprTree},
|
type_system::{Context, ReprTree},
|
||||||
tree::{TreeNav, TreeCursor, TreeNavResult},
|
tree::{TreeNav, TreeCursor, TreeNavResult},
|
||||||
diagnostics::{Diagnostics, Message},
|
diagnostics::{Diagnostics, Message},
|
||||||
tree::NestedNode,
|
tree::NestedNode,
|
||||||
|
|
|
@ -3,7 +3,7 @@ use {
|
||||||
view::{singleton::*}
|
view::{singleton::*}
|
||||||
},
|
},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{ReprTree},
|
type_system::{Context, ReprTree},
|
||||||
editors::{list::{ListEditor, ListCmd, ListCursorMode}},
|
editors::{list::{ListEditor, ListCmd, ListCursorMode}},
|
||||||
tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor},
|
tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor},
|
||||||
commander::ObjCommander
|
commander::ObjCommander
|
||||||
|
@ -20,7 +20,7 @@ impl ObjCommander for TypeTermEditor {
|
||||||
let cmd_obj = co.clone();
|
let cmd_obj = co.clone();
|
||||||
let cmd_obj = cmd_obj.read().unwrap();
|
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::<dyn SingletonView<Item = char>>() {
|
if let Some(cmd_view) = cmd_obj.get_view::<dyn SingletonView<Item = char>>() {
|
||||||
let c = cmd_view.get();
|
let c = cmd_view.get();
|
||||||
|
|
||||||
|
@ -231,11 +231,11 @@ impl ObjCommander for TypeTermEditor {
|
||||||
match &self.state {
|
match &self.state {
|
||||||
State::Any => {
|
State::Any => {
|
||||||
let cmd_repr = co.read().unwrap();
|
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::<dyn SingletonView<Item = NestedNode>>() {
|
if let Some(view) = cmd_repr.get_view::<dyn SingletonView<Item = NestedNode>>() {
|
||||||
let node = view.get();
|
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 );
|
self.set_state( State::AnySymbol );
|
||||||
} else {
|
} else {
|
||||||
self.set_state( State::Ladder );
|
self.set_state( State::Ladder );
|
||||||
|
|
|
@ -2,8 +2,9 @@ use {
|
||||||
r3vi::{
|
r3vi::{
|
||||||
view::{OuterViewPort, singleton::*}
|
view::{OuterViewPort, singleton::*}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm, MorphismTypePattern},
|
type_system::{Context, MorphismTypePattern},
|
||||||
terminal::{TerminalStyle, TerminalProjections},
|
terminal::{TerminalStyle, TerminalProjections},
|
||||||
editors::{
|
editors::{
|
||||||
list::{PTYListStyle, PTYListController, ListEditor, ListSegmentSequence},
|
list::{PTYListStyle, PTYListController, ListEditor, ListSegmentSequence},
|
||||||
|
|
|
@ -9,8 +9,9 @@ use {
|
||||||
view::{OuterViewPort, singleton::*},
|
view::{OuterViewPort, singleton::*},
|
||||||
buffer::{singleton::*}
|
buffer::{singleton::*}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeID, TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeID, TypeTerm, ReprTree},
|
type_system::{Context, ReprTree},
|
||||||
editors::{list::{ListCursorMode, ListEditor, ListCmd}},
|
editors::{list::{ListCursorMode, ListEditor, ListCmd}},
|
||||||
tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor},
|
tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor},
|
||||||
commander::ObjCommander
|
commander::ObjCommander
|
||||||
|
@ -80,7 +81,7 @@ impl TypeTermEditor {
|
||||||
|
|
||||||
node.send_cmd_obj(
|
node.send_cmd_obj(
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&ctx, "( NestedNode )"),
|
Context::parse(&ctx, "NestedNode"),
|
||||||
SingletonBuffer::new(arg_node).get_port().into()
|
SingletonBuffer::new(arg_node).get_port().into()
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
@ -98,7 +99,7 @@ impl TypeTermEditor {
|
||||||
|
|
||||||
node.send_cmd_obj(
|
node.send_cmd_obj(
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&ctx, "( NestedNode )"),
|
Context::parse(&ctx, "NestedNode"),
|
||||||
SingletonBuffer::new(arg_node).get_port().into()
|
SingletonBuffer::new(arg_node).get_port().into()
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
@ -132,37 +133,37 @@ impl TypeTermEditor {
|
||||||
fn set_state(&mut self, new_state: State) {
|
fn set_state(&mut self, new_state: State) {
|
||||||
let mut node = match new_state {
|
let mut node = match new_state {
|
||||||
State::Any => {
|
State::Any => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "<List Char>"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::Sym )").into() )
|
.morph( Context::parse(&self.ctx, "Type::Sym") )
|
||||||
}
|
}
|
||||||
State::App => {
|
State::App => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( List Type )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "<List Type>"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::App )").into() )
|
.morph( Context::parse(&self.ctx, "Type::App") )
|
||||||
}
|
}
|
||||||
State::Ladder => {
|
State::Ladder => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( List Type )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "<List Type>"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::Ladder )").into() )
|
.morph( Context::parse(&self.ctx, "Type::Ladder") )
|
||||||
}
|
}
|
||||||
State::AnySymbol => {
|
State::AnySymbol => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "<List Char>"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::Sym )").into() )
|
.morph( Context::parse(&self.ctx, "Type::Sym") )
|
||||||
},
|
},
|
||||||
State::FunSymbol => {
|
State::FunSymbol => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "<List Char>"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::Sym::Fun )").into() )
|
.morph( Context::parse(&self.ctx, "Type::Sym::Fun") )
|
||||||
},
|
},
|
||||||
State::VarSymbol => {
|
State::VarSymbol => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( List Char )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "<List Char>"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::Sym::Var )").into() )
|
.morph( Context::parse(&self.ctx, "Type::Sym::Var") )
|
||||||
}
|
}
|
||||||
State::Num => {
|
State::Num => {
|
||||||
crate::editors::integer::PosIntEditor::new(self.ctx.clone(), 10)
|
crate::editors::integer::PosIntEditor::new(self.ctx.clone(), 10)
|
||||||
.into_node()
|
.into_node()
|
||||||
.morph( (&self.ctx, "( Type::Lit::Num )").into() )
|
.morph( Context::parse(&self.ctx, "Type::Lit::Num") )
|
||||||
}
|
}
|
||||||
State::Char => {
|
State::Char => {
|
||||||
Context::make_node( &self.ctx, (&self.ctx, "( Char )").into(), self.depth.map(|x| x) ).unwrap()
|
Context::make_node( &self.ctx, Context::parse(&self.ctx, "Char"), self.depth.map(|x| x) ).unwrap()
|
||||||
.morph( (&self.ctx, "( Type::Lit::Char )").into() )
|
.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('~');
|
||||||
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();
|
let mut symb_node = Context::make_node( &ctx, Context::parse(&ctx, "<List Char>"), depth ).unwrap();
|
||||||
symb_node = symb_node.morph( (&ctx, "( Type::Sym )").into() );
|
symb_node = symb_node.morph( Context::parse(&ctx, "Type::Sym") );
|
||||||
|
|
||||||
Self::with_node(
|
Self::with_node(
|
||||||
ctx.clone(),
|
ctx.clone(),
|
||||||
|
@ -193,7 +194,7 @@ impl TypeTermEditor {
|
||||||
let buf = SingletonBuffer::<TypeTerm>::new( TypeTerm::unit() );
|
let buf = SingletonBuffer::<TypeTerm>::new( TypeTerm::unit() );
|
||||||
|
|
||||||
let data = Arc::new(RwLock::new(ReprTree::new(
|
let data = Arc::new(RwLock::new(ReprTree::new(
|
||||||
(&ctx, "( Type )")
|
Context::parse(&ctx, "Type")
|
||||||
)));
|
)));
|
||||||
|
|
||||||
let editor = TypeTermEditor {
|
let editor = TypeTermEditor {
|
||||||
|
@ -307,7 +308,7 @@ impl TypeTermEditor {
|
||||||
if subladder_list_edit.data.len() == 1 {
|
if subladder_list_edit.data.len() == 1 {
|
||||||
let it_node = subladder_list_edit.data.get(0);
|
let it_node = subladder_list_edit.data.get(0);
|
||||||
let it_node = it_node.read().unwrap();
|
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::<TypeTermEditor>().unwrap();
|
let other_tt = it_node.get_edit::<TypeTermEditor>().unwrap();
|
||||||
|
|
||||||
let mut other_tt = other_tt.write().unwrap();
|
let mut other_tt = other_tt.write().unwrap();
|
||||||
|
@ -384,7 +385,7 @@ impl TypeTermEditor {
|
||||||
self.goto(TreeCursor::home());
|
self.goto(TreeCursor::home());
|
||||||
self.send_child_cmd(
|
self.send_child_cmd(
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&self.ctx, "( NestedNode )"),
|
Context::parse(&self.ctx, "NestedNode"),
|
||||||
SingletonBuffer::new( old_edit_node ).get_port().into()
|
SingletonBuffer::new( old_edit_node ).get_port().into()
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
|
@ -21,10 +21,10 @@ use {
|
||||||
cgmath::Vector2,
|
cgmath::Vector2,
|
||||||
};
|
};
|
||||||
|
|
||||||
#[derive(Clone, Copy, Eq, PartialEq)]
|
#[derive(Clone, Copy, Eq, PartialEq, Debug)]
|
||||||
pub enum TreeNavResult { Continue, Exit }
|
pub enum TreeNavResult { Continue, Exit }
|
||||||
|
|
||||||
#[derive(Clone, Copy, Eq, PartialEq)]
|
#[derive(Clone, Copy, Eq, PartialEq, Debug)]
|
||||||
pub enum TreeHeightOp { P, Q, Max }
|
pub enum TreeHeightOp { P, Q, Max }
|
||||||
|
|
||||||
pub trait TreeNav {
|
pub trait TreeNav {
|
||||||
|
|
|
@ -5,8 +5,9 @@ use {
|
||||||
view::{View, ViewPort, OuterViewPort, AnyOuterViewPort, singleton::*, sequence::*},
|
view::{View, ViewPort, OuterViewPort, AnyOuterViewPort, singleton::*, sequence::*},
|
||||||
buffer::{singleton::*}
|
buffer::{singleton::*}
|
||||||
},
|
},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{ReprTree, Context, TypeTerm},
|
type_system::{ReprTree, Context},
|
||||||
terminal::{TerminalView, TerminalEvent, TerminalEditor, TerminalEditorResult, TerminalAtom},
|
terminal::{TerminalView, TerminalEvent, TerminalEditor, TerminalEditorResult, TerminalAtom},
|
||||||
diagnostics::{Diagnostics, Message},
|
diagnostics::{Diagnostics, Message},
|
||||||
tree::{TreeNav, TreeCursor, TreeNavResult, TreeHeightOp},
|
tree::{TreeNav, TreeCursor, TreeNavResult, TreeHeightOp},
|
||||||
|
@ -124,7 +125,7 @@ impl NestedNode {
|
||||||
NestedNode::new(
|
NestedNode::new(
|
||||||
ctx.clone(),
|
ctx.clone(),
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(&ctx, "( Char )"),
|
Context::parse(&ctx, "Char"),
|
||||||
buf.get_port().into()
|
buf.get_port().into()
|
||||||
),
|
),
|
||||||
SingletonBuffer::new(0).get_port()
|
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<Item = &'a str>) -> Option<OuterViewPort<V>>
|
pub fn get_data_port<'a, V: View + ?Sized + 'static>(&'a self, type_str: impl Iterator<Item = &'a str>) -> Option<OuterViewPort<V>>
|
||||||
where V::Msg: Clone {
|
where V::Msg: Clone {
|
||||||
let ctx = self.ctx.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)?;
|
let repr_tree = ReprTree::descend_ladder(&self.data, type_ladder)?;
|
||||||
repr_tree.clone().read().unwrap()
|
repr_tree.clone().read().unwrap()
|
||||||
|
@ -256,7 +257,7 @@ impl TerminalEditor for NestedNode {
|
||||||
if let Some(cmd) = self.cmd.get() {
|
if let Some(cmd) = self.cmd.get() {
|
||||||
cmd.write().unwrap().send_cmd_obj(
|
cmd.write().unwrap().send_cmd_obj(
|
||||||
ReprTree::new_leaf(
|
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())
|
AnyOuterViewPort::from(buf.get_port())
|
||||||
));
|
));
|
||||||
}
|
}
|
||||||
|
|
|
@ -1,7 +1,7 @@
|
||||||
|
|
||||||
use {
|
use {
|
||||||
|
laddertypes::{TypeTerm, TypeID},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeTerm, TypeID},
|
|
||||||
tree::{TreeAddr}
|
tree::{TreeAddr}
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
|
@ -1,7 +1,8 @@
|
||||||
use {
|
use {
|
||||||
r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}},
|
r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}},
|
||||||
|
laddertypes::{TypeDict, TypeTerm, TypeID},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeDict, TypeTerm, TypeID, ReprTree},
|
type_system::{ReprTree},
|
||||||
tree::NestedNode
|
tree::NestedNode
|
||||||
},
|
},
|
||||||
std::{
|
std::{
|
||||||
|
@ -135,12 +136,6 @@ impl Default for Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl Into<TypeTerm> for (&Arc<RwLock<Context>>, &str) {
|
|
||||||
fn into(self) -> TypeTerm {
|
|
||||||
self.0.read().unwrap().type_term_from_str(self.1).expect("could not parse type term")
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl Context {
|
impl Context {
|
||||||
pub fn with_parent(parent: Option<Arc<RwLock<Context>>>) -> Self {
|
pub fn with_parent(parent: Option<Arc<RwLock<Context>>>) -> Self {
|
||||||
Context {
|
Context {
|
||||||
|
@ -174,6 +169,10 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn parse(ctx: &Arc<RwLock<Self>>, 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 {
|
pub fn add_typename(&mut self, tn: &str) -> TypeID {
|
||||||
self.type_dict.write().unwrap().add_typename(tn.to_string())
|
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<TypeTerm> {
|
pub fn type_term_from_str(&self, tn: &str) -> Result<TypeTerm, laddertypes::parser::ParseError> {
|
||||||
self.type_dict.read().unwrap().type_term_from_str(&tn)
|
self.type_dict.write().unwrap().parse(&tn)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn type_term_to_str(&self, t: &TypeTerm) -> String {
|
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<dyn Fn(Arc<RwLock<Self>>, TypeTerm, OuterViewPort<dyn SingletonView<Item = usize>>) -> Option<NestedNode> + Send + Sync>) {
|
pub fn add_node_ctor(&mut self, tn: &str, mk_editor: Arc<dyn Fn(Arc<RwLock<Self>>, TypeTerm, OuterViewPort<dyn SingletonView<Item = usize>>) -> Option<NestedNode> + Send + Sync>) {
|
||||||
|
@ -332,8 +331,8 @@ impl Context {
|
||||||
/// adds an object without any representations
|
/// adds an object without any representations
|
||||||
pub fn add_obj(ctx: Arc<RwLock<Context>>, name: String, typename: &str) {
|
pub fn add_obj(ctx: Arc<RwLock<Context>>, name: String, typename: &str) {
|
||||||
let type_tag = ctx.read().unwrap()
|
let type_tag = ctx.read().unwrap()
|
||||||
.type_dict.read().unwrap()
|
.type_dict.write().unwrap()
|
||||||
.type_term_from_str(typename).unwrap();
|
.parse(typename).unwrap();
|
||||||
|
|
||||||
if let Some(node) = Context::make_node(&ctx, type_tag, SingletonBuffer::new(0).get_port()) {
|
if let Some(node) = Context::make_node(&ctx, type_tag, SingletonBuffer::new(0).get_port()) {
|
||||||
ctx.write().unwrap().nodes.insert(name, node);
|
ctx.write().unwrap().nodes.insert(name, node);
|
||||||
|
|
|
@ -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<String, TypeID>,
|
|
||||||
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<String> {
|
|
||||||
self.typenames.my.get(tid).cloned()
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
|
|
||||||
self.typenames.mλ.get(tn).cloned()
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn type_term_from_str(&self, typename: &str) -> Option<TypeTerm> {
|
|
||||||
TypeTerm::from_str(typename, &self.typenames.mλ)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn type_term_to_str(&self, term: &TypeTerm) -> String {
|
|
||||||
term.to_str(&self.typenames.my)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
|
@ -1,71 +0,0 @@
|
||||||
use {
|
|
||||||
crate::type_system::{TypeTerm, TypeID},
|
|
||||||
std::collections::HashMap
|
|
||||||
};
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
#[derive(Clone, Eq, PartialEq, Hash, Debug)]
|
|
||||||
pub struct TypeLadder(pub Vec<TypeTerm>);
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
||||||
impl From<Vec<TypeTerm>> for TypeLadder {
|
|
||||||
fn from(l: Vec<TypeTerm>) -> Self {
|
|
||||||
TypeLadder(l)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl From<TypeTerm> 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<usize> {
|
|
||||||
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<usize, Option<(usize, usize)>> {
|
|
||||||
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<TypeID, String>) -> 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
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
||||||
|
|
|
@ -1,15 +1,8 @@
|
||||||
pub mod context;
|
pub mod context;
|
||||||
|
|
||||||
pub mod dict;
|
|
||||||
pub mod term;
|
|
||||||
//pub mod ladder;
|
|
||||||
pub mod repr_tree;
|
pub mod repr_tree;
|
||||||
|
|
||||||
pub use {
|
pub use {
|
||||||
dict::*,
|
context::{Context, MorphismMode, MorphismType, MorphismTypePattern},
|
||||||
// ladder::*,
|
repr_tree::ReprTree
|
||||||
repr_tree::*,
|
|
||||||
term::*,
|
|
||||||
context::{Context, MorphismMode, MorphismType, MorphismTypePattern}
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -1,7 +1,8 @@
|
||||||
use {
|
use {
|
||||||
r3vi::view::{AnyOuterViewPort, OuterViewPort, View},
|
r3vi::view::{AnyOuterViewPort, OuterViewPort, View},
|
||||||
|
laddertypes::{TypeTerm},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeTerm, Context}
|
type_system::{Context}
|
||||||
},
|
},
|
||||||
std::{
|
std::{
|
||||||
collections::HashMap,
|
collections::HashMap,
|
||||||
|
@ -50,7 +51,7 @@ impl ReprTree {
|
||||||
pub fn from_char(ctx: &Arc<RwLock<Context>>, c: char) -> Arc<RwLock<Self>> {
|
pub fn from_char(ctx: &Arc<RwLock<Context>>, c: char) -> Arc<RwLock<Self>> {
|
||||||
let buf = r3vi::buffer::singleton::SingletonBuffer::<char>::new(c);
|
let buf = r3vi::buffer::singleton::SingletonBuffer::<char>::new(c);
|
||||||
ReprTree::new_leaf(
|
ReprTree::new_leaf(
|
||||||
(ctx, "( Char )"),
|
Context::parse(ctx, "Char"),
|
||||||
buf.get_port().into()
|
buf.get_port().into()
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
|
@ -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<TypeTerm>) -> &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<TypeTerm> {
|
|
||||||
match self.normalize() {
|
|
||||||
TypeTerm::Ladder( v ) => {
|
|
||||||
v
|
|
||||||
},
|
|
||||||
_ => {
|
|
||||||
unreachable!();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
/// transmute self into Ladder-Normal-Form
|
|
||||||
///
|
|
||||||
/// Example:
|
|
||||||
/// <Seq <Digit 10>~Char> ⇒ <Seq <Digit 10>>~<Seq Char>
|
|
||||||
pub fn normalize(self) -> Self {
|
|
||||||
let mut new_ladder = Vec::<TypeTerm>::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<usize, Option<(usize, usize)>> {
|
|
||||||
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<String, TypeID>) -> Option<Self> {
|
|
||||||
let mut term_stack = Vec::<Option<TypeTerm>>::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<TypeID, String>) -> 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]),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
Loading…
Reference in a new issue