upgrade node with morphisms

This commit is contained in:
Michael Sippel 2023-02-17 00:59:07 +01:00
parent 6f942c8940
commit 2bdea3e2a3
Signed by: senvas
GPG key ID: F96CF119C34B64A6
14 changed files with 220 additions and 113 deletions

View file

@ -103,7 +103,7 @@ impl ListEditor {
pub fn get_seq_type(&self) -> TypeTerm { pub fn get_seq_type(&self) -> TypeTerm {
TypeTerm::Type { TypeTerm::Type {
id: self.ctx.read().unwrap().get_typeid("Sequence").unwrap(), id: self.ctx.read().unwrap().get_typeid("List").unwrap(),
args: vec![ self.get_item_type() ] args: vec![ self.get_item_type() ]
} }
} }
@ -277,4 +277,24 @@ impl ListEditor {
} }
} }
} }
/*
use crate::{
type_system::TypeLadder,
tree::{TreeType, TreeAddr}
};
impl TreeType for ListEditor {
fn get_type(&self, addr: &TreeAddr) -> TypeLadder {
let idx = crate::utils::modulo::modulo(addr.0[0] as isize, self.data.len() as isize) as usize;
let mut addr = addr.clone();
if self.data.len() > 0 {
addr.0.remove(0);
self.data.get(idx).get_type(addr)
} else {
vec![]
}
}
}
*/

View file

@ -19,7 +19,7 @@ use {
make_label make_label
}, },
tree::{TreeCursor, TreeNav}, tree::{TreeCursor, TreeNav},
diagnostics::{Diagnostics, make_error}, diagnostics::{Diagnostics},
tree::NestedNode, tree::NestedNode,
commander::Commander, commander::Commander,
PtySegment PtySegment
@ -180,7 +180,6 @@ impl PTYListEditor {
let ed = editor.read().unwrap(); let ed = editor.read().unwrap();
let edd = ed.editor.read().unwrap(); let edd = ed.editor.read().unwrap();
NestedNode::new() NestedNode::new()
.set_data(edd.get_data()) .set_data(edd.get_data())
.set_cmd(editor.clone()) .set_cmd(editor.clone())
@ -354,7 +353,7 @@ impl Commander for PTYListEditor {
e.delete_nexd(); e.delete_nexd();
} }
_ => { _ => {
let mut new_edit = Context::make_editor(&e.ctx, e.typ.clone(), self.depth).unwrap(); let mut new_edit = Context::make_node(&e.ctx, e.typ.clone(), self.depth).unwrap();
new_edit.goto(TreeCursor::home()); new_edit.goto(TreeCursor::home());
new_edit.handle_terminal_event(event); new_edit.handle_terminal_event(event);

View file

@ -235,7 +235,7 @@ impl TerminalEditor for ProductEditor {
} }
} }
} else { } else {
let mut e = Context::make_editor(&self.ctx, t[0].clone(), *ed_depth+1).unwrap(); let mut e = Context::make_node(&self.ctx, t[0].clone(), *ed_depth+1).unwrap();
*editor = Some(e.clone()); *editor = Some(e.clone());
update_segment = true; update_segment = true;

View file

@ -71,7 +71,7 @@ impl TreeNav for ProductEditor {
e.goto(c.clone()); e.goto(c.clone());
} else if c.tree_addr.len() > 0 { } else if c.tree_addr.len() > 0 {
// create editor // create editor
let mut e = Context::make_editor(&self.ctx, t[0].clone(), *ed_depth+1).unwrap(); let mut e = Context::make_node(&self.ctx, t[0].clone(), *ed_depth+1).unwrap();
*editor = Some(e.clone()); *editor = Some(e.clone());
e.goto(c.clone()); e.goto(c.clone());
} }
@ -128,7 +128,7 @@ impl TreeNav for ProductEditor {
} else { } else {
// create editor // create editor
let mut e = Context::make_editor(&self.ctx, t[0].clone(), *ed_depth+1).unwrap(); let mut e = Context::make_node(&self.ctx, t[0].clone(), *ed_depth+1).unwrap();
*editor = Some(e.clone()); *editor = Some(e.clone());
e.goby(direction); e.goby(direction);
} }

View file

@ -3,9 +3,6 @@ use {
view::{ view::{
ViewPort, OuterViewPort, ViewPort, OuterViewPort,
sequence::*, sequence::*,
},
buffer::{
vec::*
} }
}, },
crate::{ crate::{

View file

@ -1,5 +1,5 @@
pub struct TreeAddr(Vec<usize>); pub struct TreeAddr(pub Vec<usize>);
impl From<Vec<usize>> for TreeAddr { impl From<Vec<usize>> for TreeAddr {
fn from(v: Vec<usize>) -> TreeAddr { fn from(v: Vec<usize>) -> TreeAddr {

View file

@ -2,11 +2,13 @@ pub mod addr;
pub mod cursor; pub mod cursor;
pub mod nav; pub mod nav;
pub mod node; pub mod node;
pub mod treetype;
pub use { pub use {
addr::TreeAddr, addr::TreeAddr,
cursor::TreeCursor, cursor::TreeCursor,
nav::{TreeNav, TreeNavResult}, nav::{TreeNav, TreeNavResult},
treetype::{TreeType},
node::NestedNode node::NestedNode
}; };

View file

@ -52,6 +52,17 @@ impl ObjCommander for NestedNode {
} }
} }
/*
impl TreeType for NestedNode {
fn get_type(&self, addr: &TreeAddr) -> TypeLadder {
if let Some(editor) = self.editor {
editor.read().unwrap().get_type(addr)
} else {
vec![]
}
}
}
*/
// todo: remove that at some point // todo: remove that at some point
impl TerminalEditor for NestedNode { impl TerminalEditor for NestedNode {
fn get_term_view(&self) -> OuterViewPort<dyn TerminalView> { fn get_term_view(&self) -> OuterViewPort<dyn TerminalView> {

View file

@ -0,0 +1,14 @@
use {
crate::{
type_system::TypeLadder,
tree::{TreeAddr}
}
};
pub trait TreeType {
fn get_type(&self, _addr: &TreeAddr) -> TypeLadder {
vec![]
}
}

View file

@ -35,29 +35,50 @@ pub enum MorphismMode {
#[derive(Clone, Hash, PartialEq, Eq)] #[derive(Clone, Hash, PartialEq, Eq)]
pub struct MorphismType { pub struct MorphismType {
pub mode: MorphismMode, // pub mode: MorphismMode,
pub src_type: TypeTerm, pub src_type: Option<TypeTerm>,
pub dst_type: TypeTerm, pub dst_type: TypeTerm,
} }
#[derive(Hash, Eq, PartialEq, Debug)]
pub struct MorphismTypePattern {
pub src_type: Option<TypeTerm>,
pub dst_tyid: TypeID
}
impl From<MorphismType> for MorphismTypePattern {
fn from(value: MorphismType) -> MorphismTypePattern {
MorphismTypePattern {
src_type: value.src_type,
dst_tyid: match value.dst_type {
TypeTerm::Type { id, args: _ } => id,
_ => unreachable!()
}
}
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
pub struct Context { pub struct Context {
/// assigns a name to every type /// assigns a name to every type
type_dict: Arc<RwLock<TypeDict>>, type_dict: Arc<RwLock<TypeDict>>,
/// objects /// vertices of the graph
objects: HashMap<String, Arc<RwLock<ReprTree>>>, nodes: HashMap< String, NestedNode >,
/// todo: beautify
/// types that can be edited as lists /// types that can be edited as lists
list_types: Vec<TypeID>, list_types: Vec< TypeID >,
/// editors /// graph constructors
editor_ctors: HashMap<TypeID, Arc<dyn Fn(Arc<RwLock<Self>>, TypeTerm, usize) -> Option<NestedNode> + Send + Sync>>, morphisms: HashMap<
MorphismTypePattern,
/// morphisms Arc<
default_constructors: HashMap<TypeTerm, Box<dyn Fn() -> Arc<RwLock<ReprTree>> + Send + Sync>>, dyn Fn( NestedNode, TypeTerm, usize ) -> Option<NestedNode>
morphism_constructors: HashMap<MorphismType, Box<dyn Fn(Arc<RwLock<ReprTree>>) -> Arc<RwLock<ReprTree>> + Send + Sync>>, + Send + Sync
>
>,
/// recursion /// recursion
parent: Option<Arc<RwLock<Context>>>, parent: Option<Arc<RwLock<Context>>>,
@ -70,10 +91,8 @@ impl Context {
Some(p) => p.read().unwrap().type_dict.clone(), Some(p) => p.read().unwrap().type_dict.clone(),
None => Arc::new(RwLock::new(TypeDict::new())) None => Arc::new(RwLock::new(TypeDict::new()))
}, },
editor_ctors: HashMap::new(), morphisms: HashMap::new(),
default_constructors: HashMap::new(), nodes: HashMap::new(),
morphism_constructors: HashMap::new(),
objects: HashMap::new(),
list_types: match parent.as_ref() { list_types: match parent.as_ref() {
Some(p) => p.read().unwrap().list_types.clone(), Some(p) => p.read().unwrap().list_types.clone(),
None => Vec::new() None => Vec::new()
@ -86,6 +105,14 @@ impl Context {
Context::with_parent(None) Context::with_parent(None)
} }
pub fn depth(&self) -> usize {
if let Some(parent) = self.parent.as_ref() {
parent.read().unwrap().depth() + 1
} else {
0
}
}
pub fn add_typename(&mut self, tn: String) -> TypeID { pub fn add_typename(&mut self, tn: String) -> TypeID {
self.type_dict.write().unwrap().add_typename(tn) self.type_dict.write().unwrap().add_typename(tn)
} }
@ -116,73 +143,97 @@ impl Context {
self.type_dict.read().unwrap().type_term_to_str(&t) self.type_dict.read().unwrap().type_term_to_str(&t)
} }
pub fn add_editor_ctor(&mut self, tn: &str, mk_editor: Arc<dyn Fn(Arc<RwLock<Self>>, TypeTerm, usize) -> Option<NestedNode> + Send + Sync>) { pub fn add_node_ctor(&mut self, tn: &str, mk_editor: Arc<dyn Fn(Arc<RwLock<Self>>, TypeTerm, usize) -> Option<NestedNode> + Send + Sync>) {
let mut dict = self.type_dict.write().unwrap(); let dict = self.type_dict.clone();
let mut dict = dict.write().unwrap();
let tyid = let tyid =
if let Some(tyid) = dict.get_typeid(&tn.into()) { if let Some(tyid) = dict.get_typeid(&tn.into()) {
tyid tyid
} else { } else {
dict.add_typename(tn.into()) dict.add_typename(tn.into())
}; };
self.editor_ctors.insert(tyid, mk_editor);
let morphism_pattern = MorphismTypePattern {
src_type: None,
dst_tyid: tyid
};
self.add_morphism(morphism_pattern, Arc::new(move |node, dst_type, depth| {
let ctx = node.ctx.clone().unwrap();
mk_editor(ctx, dst_type, depth)
}));
} }
pub fn get_editor_ctor(&self, ty: &TypeTerm) -> Option<Arc<dyn Fn(Arc<RwLock<Self>>, TypeTerm, usize) -> Option<NestedNode> + Send + Sync>> { pub fn add_morphism(
if let TypeTerm::Type{ id, args: _ } = ty.clone() { &mut self,
if let Some(m) = self.editor_ctors.get(&id).cloned() { morph_type_pattern: MorphismTypePattern,
Some(m) morph_fn: Arc<
dyn Fn( NestedNode, TypeTerm, usize ) -> Option<NestedNode>
+ Send + Sync
>
) {
self.morphisms.insert(morph_type_pattern, morph_fn);
}
pub fn get_morphism(&self, ty: MorphismType) -> Option<Arc<dyn Fn(NestedNode, TypeTerm, usize) -> Option<NestedNode> + Send + Sync>> {
let pattern = MorphismTypePattern::from(ty.clone());
if let Some(morphism) = self.morphisms.get( &pattern ) {
Some(morphism.clone())
} else { } else {
self.parent.as_ref()? self.parent.as_ref()?
.read().unwrap() .read().unwrap()
.get_editor_ctor(&ty) .get_morphism(ty)
}
} else {
None
} }
} }
pub fn make_editor(ctx: &Arc<RwLock<Self>>, type_term: TypeTerm, depth: usize) -> Option<NestedNode> { pub fn make_node(ctx: &Arc<RwLock<Self>>, type_term: TypeTerm, depth: usize) -> Option<NestedNode> {
let mk_editor = ctx.read().unwrap().get_editor_ctor(&type_term)?; let mk_node = ctx.read().unwrap().get_morphism(MorphismType {
mk_editor(ctx.clone(), type_term, depth) src_type: None,
} dst_type: type_term.clone()
/* })?;
pub fn enrich_editor(
node: NestedNode,
typ: TypeTerm
) -> NestedNode {
mk_node(NestedNode::new().set_ctx(ctx.clone()), type_term, depth)
// create view
// create commander
}
*/
pub fn add_morphism(
&mut self,
morph_type: MorphismType,
morph_fn: Box<dyn Fn(Arc<RwLock<ReprTree>>) -> Arc<RwLock<ReprTree>> + Send + Sync>,
) {
self.morphism_constructors.insert(morph_type, morph_fn);
} }
/// adds an object without any representations pub fn morph_node(ctx: Arc<RwLock<Self>>, mut node: NestedNode, dst_type: TypeTerm) -> NestedNode {
pub fn add_obj(&mut self, name: String, typename: &str) { let mut src_type = None;
let type_tag = self.type_dict.read().unwrap().type_term_from_str(typename).unwrap();
self.objects.insert( if let Some(data) = node.data.clone() {
name, src_type = Some(data.read().unwrap().get_type().clone());
if let Some(ctor) = self.default_constructors.get(&type_tag) { node = node.set_data(
ctor() ReprTree::ascend(
} else { &data,
Arc::new(RwLock::new(ReprTree::new(type_tag))) dst_type.clone()
}, )
); );
} }
pub fn get_obj(&self, name: &String) -> Option<Arc<RwLock<ReprTree>>> { let pattern = MorphismType { src_type, dst_type: dst_type.clone() }.into();
if let Some(obj) = self.objects.get(name) { if let Some(transform) = ctx.read().unwrap().get_morphism(pattern) {
if let Some(new_node) = transform(node.clone(), dst_type, 0) {
new_node
} else {
node.clone()
}
} else {
node
}
}
/// adds an object without any representations
pub fn add_obj(ctx: Arc<RwLock<Context>>, name: String, typename: &str) {
let type_tag = ctx.read().unwrap()
.type_dict.read().unwrap()
.type_term_from_str(typename).unwrap();
if let Some(node) = Context::make_node(&ctx, type_tag, 0) {
ctx.write().unwrap().nodes.insert(name, node);
}
}
pub fn get_obj(&self, name: &String) -> Option<NestedNode> {
if let Some(obj) = self.nodes.get(name) {
Some(obj.clone()) Some(obj.clone())
} else if let Some(parent) = self.parent.as_ref() { } else if let Some(parent) = self.parent.as_ref() {
parent.read().unwrap().get_obj(name) parent.read().unwrap().get_obj(name)

View file

@ -11,7 +11,7 @@ use {
tree::{NestedNode}, tree::{NestedNode},
terminal::{TerminalEditor}, terminal::{TerminalEditor},
diagnostics::{Diagnostics}, diagnostics::{Diagnostics},
type_system::TypeTermEditor, type_system::{TypeTermEditor, MorphismTypePattern},
}, },
std::sync::{Arc, RwLock}, std::sync::{Arc, RwLock},
cgmath::Point2 cgmath::Point2
@ -28,7 +28,7 @@ pub fn init_mem_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
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))));
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"Char", Arc::new( "Char", Arc::new(
|ctx: Arc<RwLock<Context>>, _ty: TypeTerm, _depth: usize| { |ctx: Arc<RwLock<Context>>, _ty: TypeTerm, _depth: usize| {
Some(CharEditor::new_node(&ctx)) Some(CharEditor::new_node(&ctx))
@ -38,7 +38,7 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
ctx.write().unwrap().add_list_typename("Sequence".into()); ctx.write().unwrap().add_list_typename("Sequence".into());
ctx.write().unwrap().add_list_typename("List".into()); ctx.write().unwrap().add_list_typename("List".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"List", Arc::new( "List", Arc::new(
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| { |ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| {
match ty { match ty {
@ -65,20 +65,44 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
); );
ctx.write().unwrap().add_list_typename("Symbol".into()); ctx.write().unwrap().add_list_typename("Symbol".into());
ctx.write().unwrap().add_editor_ctor(
"Symbol", Arc::new(
|ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| {
let mut node = PTYListEditor::new(
ctx.clone(),
ctx.read().unwrap().type_term_from_str("( Char )").unwrap(),
ListStyle::Plain,
depth + 1
).into_node();
node.data = Some(ReprTree::ascend( let pattern = MorphismTypePattern {
&node.data.unwrap(), src_type: ctx.read().unwrap().type_term_from_str("( List Char )"),
ctx.read().unwrap().type_term_from_str("( Symbol )").unwrap() dst_tyid: ctx.read().unwrap().get_typeid("Symbol").unwrap()
)); };
ctx.write().unwrap().add_morphism(pattern,
Arc::new(
|mut node, dst_type:_, depth| {
let editor = node.editor.clone().unwrap().downcast::<RwLock<ListEditor>>().unwrap();
let pty_editor = PTYListEditor::from_editor(
editor,
ListStyle::Plain,
depth
);
node.view = Some(pty_editor.pty_view());
node.cmd = Some(Arc::new(RwLock::new(pty_editor)));
Some(node)
}
)
);
ctx.write().unwrap().add_node_ctor(
"Symbol", Arc::new(
|ctx: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
let mut node = Context::make_node(
&ctx,
TypeTerm::Type {
id: ctx.read().unwrap().get_typeid("List").unwrap(),
args: vec![
TypeTerm::new(ctx.read().unwrap().get_typeid("Char").unwrap())
]
},
depth
).unwrap();
node = Context::morph_node(ctx, node, dst_typ);
Some(node) Some(node)
} }
@ -86,7 +110,7 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
); );
ctx.write().unwrap().add_list_typename("String".into()); ctx.write().unwrap().add_list_typename("String".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"String", Arc::new( "String", Arc::new(
|ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| { |ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| {
let mut node = PTYListEditor::new( let mut node = PTYListEditor::new(
@ -107,7 +131,7 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
); );
ctx.write().unwrap().add_list_typename("TypeTerm".into()); ctx.write().unwrap().add_list_typename("TypeTerm".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"TypeTerm", Arc::new( "TypeTerm", Arc::new(
|ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| { |ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| {
Some(TypeTermEditor::new(ctx, depth).into_node()) Some(TypeTermEditor::new(ctx, depth).into_node())
@ -126,7 +150,7 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
ctx.write().unwrap().add_typename("u32".into()); ctx.write().unwrap().add_typename("u32".into());
ctx.write().unwrap().add_typename("BigEndian".into()); ctx.write().unwrap().add_typename("BigEndian".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"Digit", Arc::new( "Digit", Arc::new(
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, _depth: usize| { |ctx: Arc<RwLock<Context>>, ty: TypeTerm, _depth: usize| {
match ty { match ty {
@ -154,7 +178,7 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
); );
ctx.write().unwrap().add_list_typename("PosInt".into()); ctx.write().unwrap().add_list_typename("PosInt".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"PosInt", Arc::new( "PosInt", Arc::new(
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, _depth: usize| { |ctx: Arc<RwLock<Context>>, ty: TypeTerm, _depth: usize| {
match ty { match ty {
@ -181,9 +205,9 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
); );
ctx.write().unwrap().add_list_typename("RGB".into()); ctx.write().unwrap().add_list_typename("RGB".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"RGB", Arc::new( "RGB", Arc::new(
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| { |ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| {
let editor = ProductEditor::new(depth, ctx.clone()) let editor = ProductEditor::new(depth, ctx.clone())
.with_t(Point2::new(0, 0), "r: ") .with_t(Point2::new(0, 0), "r: ")
.with_n(Point2::new(1, 0), .with_n(Point2::new(1, 0),
@ -225,7 +249,7 @@ pub fn init_os_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))));
ctx.write().unwrap().add_list_typename("PathSegment".into()); ctx.write().unwrap().add_list_typename("PathSegment".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"PathSegment", Arc::new( "PathSegment", Arc::new(
|ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| { |ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| {
let mut node = PTYListEditor::new( let mut node = PTYListEditor::new(
@ -246,7 +270,7 @@ pub fn init_os_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
); );
ctx.write().unwrap().add_list_typename("Path".into()); ctx.write().unwrap().add_list_typename("Path".into());
ctx.write().unwrap().add_editor_ctor( ctx.write().unwrap().add_node_ctor(
"Path", Arc::new( "Path", Arc::new(
|ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| { |ctx: Arc<RwLock<Context>>, _ty: TypeTerm, depth: usize| {
let mut node = PTYListEditor::new( let mut node = PTYListEditor::new(

View file

@ -8,7 +8,7 @@ pub mod type_term_editor;
pub use { pub use {
repr_tree::{ReprTree}, repr_tree::{ReprTree},
type_term::{TypeDict, TypeID, TypeTerm, TypeLadder}, type_term::{TypeDict, TypeID, TypeTerm, TypeLadder},
context::{Context, MorphismMode, MorphismType}, context::{Context, MorphismMode, MorphismType, MorphismTypePattern},
type_term_editor::TypeTermEditor, type_term_editor::TypeTermEditor,
make_editor::* make_editor::*
}; };

View file

@ -7,7 +7,7 @@ pub type TypeLadder = Vec<TypeTerm>;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
#[derive(Clone, PartialEq, Eq, Hash)] #[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub enum TypeTerm { pub enum TypeTerm {
Type { id: TypeID, args: Vec<TypeTerm> }, Type { id: TypeID, args: Vec<TypeTerm> },
Num(i64), Num(i64),

View file

@ -1,26 +1,15 @@
use { use {
r3vi::{
view::{
OuterViewPort,
sequence::*
}
},
crate::{ crate::{
type_system::{Context}, type_system::{Context},
terminal::{TerminalEvent, TerminalView, TerminalEditor, TerminalEditorResult}, terminal::{TerminalEvent},
editors::{ editors::{
list::*,
sum::*, sum::*,
char::CharEditor,
integer::PosIntEditor,
}, },
tree::{TreeNav, TreeCursor, TreeNavResult}, tree::{TreeNav},
diagnostics::{Diagnostics, Message},
tree::NestedNode, tree::NestedNode,
commander::Commander, commander::Commander,
PtySegment PtySegment
}, },
cgmath::{Vector2},
termion::event::{Key}, termion::event::{Key},
std::{ std::{
sync::{Arc, RwLock} sync::{Arc, RwLock}
@ -48,9 +37,9 @@ impl TypeTermEditor {
ty: TypeTermVar::Any, ty: TypeTermVar::Any,
sum_edit: Arc::new(RwLock::new(SumEditor::new( sum_edit: Arc::new(RwLock::new(SumEditor::new(
vec![ vec![
Context::make_editor( &ctx, ctx.read().unwrap().type_term_from_str("( List TypeTerm )").unwrap(), depth + 1).unwrap(), Context::make_node( &ctx, ctx.read().unwrap().type_term_from_str("( List TypeTerm )").unwrap(), depth + 1).unwrap(),
Context::make_editor( &ctx, ctx.read().unwrap().type_term_from_str("( PosInt 10 )").unwrap(), depth + 1 ).unwrap(), Context::make_node( &ctx, ctx.read().unwrap().type_term_from_str("( PosInt 10 )").unwrap(), depth + 1 ).unwrap(),
Context::make_editor( &ctx, ctx.read().unwrap().type_term_from_str("( Symbol )").unwrap(), depth + 1 ).unwrap() Context::make_node( &ctx, ctx.read().unwrap().type_term_from_str("( Symbol )").unwrap(), depth + 1 ).unwrap()
]))) ])))
} }
} }