From 2d46ac95bdd8038d0c5ca8bd68ad9932cd693734 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sat, 12 Aug 2023 19:03:14 +0200 Subject: [PATCH] restructure TypeTerm --- nested/src/editors/integer/editor.rs | 22 +-- nested/src/editors/list/commander.rs | 8 +- nested/src/editors/list/editor.rs | 16 +-- nested/src/editors/product/editor.rs | 10 +- nested/src/editors/product/nav.rs | 4 +- nested/src/editors/product/segment.rs | 6 +- nested/src/tree/treetype.rs | 6 +- nested/src/type_system/context.rs | 30 ++-- nested/src/type_system/dict.rs | 6 +- nested/src/type_system/editor.rs | 95 ++++++++++++- nested/src/type_system/ladder.rs | 2 +- nested/src/type_system/make_editor.rs | 197 +++++++++++--------------- nested/src/type_system/mod.rs | 4 +- nested/src/type_system/repr_tree.rs | 3 +- nested/src/type_system/term.rs | 145 +++++++++++-------- 15 files changed, 312 insertions(+), 242 deletions(-) diff --git a/nested/src/editors/integer/editor.rs b/nested/src/editors/integer/editor.rs index 93f7636..410d3a0 100644 --- a/nested/src/editors/integer/editor.rs +++ b/nested/src/editors/integer/editor.rs @@ -117,12 +117,7 @@ impl DigitEditor { } pub fn get_type(&self) -> TypeTerm { - TypeTerm::Type { - id: self.ctx.read().unwrap().get_fun_typeid("Digit").unwrap(), - args: vec![ - TypeTerm::Num(self.radix as i64).into() - ] - } + TypeTerm::TypeID(self.ctx.read().unwrap().get_typeid("Digit").unwrap()) } pub fn get_data(&self) -> Arc> { @@ -163,17 +158,12 @@ impl PosIntEditor { let data = node.data.clone().unwrap(); node = node.set_data(ReprTree::ascend( &data, - TypeTerm::Type { - id: ctx.read().unwrap().get_fun_typeid("PosInt").unwrap(), - args: vec![ - TypeTerm::Num(radix as i64).into(), - TypeTerm::Type { - id: ctx.read().unwrap().get_fun_typeid("BigEndian").unwrap(), - args: vec![] - }.into() + TypeTerm::App(vec![ + TypeTerm::TypeID(ctx.read().unwrap().get_typeid("PosInt").unwrap()), + TypeTerm::Num(radix as i64).into(), + TypeTerm::TypeID(ctx.read().unwrap().get_typeid("BigEndian").unwrap()) ] - } - )); + ))); PosIntEditor { radix, diff --git a/nested/src/editors/list/commander.rs b/nested/src/editors/list/commander.rs index 438283e..874a566 100644 --- a/nested/src/editors/list/commander.rs +++ b/nested/src/editors/list/commander.rs @@ -32,7 +32,13 @@ impl ListCmd { ) } } - +/* +impl Into< Arc> > for (&Arc>, ListCmd) { + fn into(self) -> Arc> { + self.1.into_repr_tree(self.0) + } +} +*/ impl ObjCommander for ListEditor { fn send_cmd_obj(&mut self, cmd_obj: Arc>) -> TreeNavResult { let cmd_repr = cmd_obj.read().unwrap(); diff --git a/nested/src/editors/list/editor.rs b/nested/src/editors/list/editor.rs index ca36f42..23e9986 100644 --- a/nested/src/editors/list/editor.rs +++ b/nested/src/editors/list/editor.rs @@ -38,11 +38,9 @@ impl ListEditor { "List", Arc::new( |ctx: Arc>, ty: TypeTerm, depth: usize| { match ty { - TypeTerm::Type { - id: _, args - } => { - if args.len() > 0 { - let typ = (args[0].clone().0)[0].clone(); + TypeTerm::App(args) => { + if args.len() > 1 { + let typ = args[1].clone(); let mut node = ListEditor::new(ctx.clone(), typ).into_node(depth); @@ -160,10 +158,10 @@ impl ListEditor { } pub fn get_seq_type(&self) -> TypeTerm { - TypeTerm::Type { - id: self.ctx.read().unwrap().get_fun_typeid("List").unwrap(), - args: vec![ self.get_item_type().into() ] - } + TypeTerm::App(vec![ + TypeTerm::TypeID(self.ctx.read().unwrap().get_typeid("List").unwrap()), + self.get_item_type().into() + ]) } pub fn get_cursor_port(&self) -> OuterViewPort> { diff --git a/nested/src/editors/product/editor.rs b/nested/src/editors/product/editor.rs index f484dae..6e44f2e 100644 --- a/nested/src/editors/product/editor.rs +++ b/nested/src/editors/product/editor.rs @@ -10,7 +10,7 @@ use { } }, crate::{ - type_system::{TypeLadder, Context}, + type_system::{Context, TypeTerm}, terminal::{ TerminalEditor, TerminalEditorResult, TerminalEvent, TerminalView @@ -79,7 +79,7 @@ impl ProductEditor { self } - pub fn with_n(mut self, pos: Point2, n: TypeLadder) -> Self { + pub fn with_n(mut self, pos: Point2, n: &TypeTerm) -> Self { self.segments.insert(pos, ProductEditorSegment::N{ t: n.clone(), editor: None, @@ -90,7 +90,7 @@ impl ProductEditor { self.n_indices.push(pos); let mut b = VecBuffer::new(); - b.push(crate::diagnostics::make_todo(crate::terminal::make_label(&format!("complete {}", self.ctx.read().unwrap().type_term_to_str(&n.0[0]))))); + b.push(crate::diagnostics::make_todo(crate::terminal::make_label(&format!("complete {}", self.ctx.read().unwrap().type_term_to_str(n))))); self.msg_buf.push(Some(b.get_port().to_sequence())); self } @@ -157,7 +157,7 @@ impl ProductEditor { self.msg_buf.update(idx as usize, Some(e.get_msg_port())); } else { let mut b = VecBuffer::new(); - b.push(crate::diagnostics::make_todo(crate::terminal::make_label(&format!("complete {}", self.ctx.read().unwrap().type_term_to_str(&t.0[0]))))); + b.push(crate::diagnostics::make_todo(crate::terminal::make_label(&format!("complete {}", self.ctx.read().unwrap().type_term_to_str(&t))))); self.msg_buf.update(idx as usize, Some(b.get_port().to_sequence())); @@ -238,7 +238,7 @@ impl ObjCommander for ProductEditor { } } } else { - let mut e = Context::make_node(&self.ctx, t.0[0].clone(), *ed_depth+1).unwrap(); + let mut e = Context::make_node(&self.ctx, t.clone(), *ed_depth+1).unwrap(); *editor = Some(e.clone()); update_segment = true; diff --git a/nested/src/editors/product/nav.rs b/nested/src/editors/product/nav.rs index e3ba8c9..d60a8a3 100644 --- a/nested/src/editors/product/nav.rs +++ b/nested/src/editors/product/nav.rs @@ -71,7 +71,7 @@ impl TreeNav for ProductEditor { e.goto(c.clone()); } else if c.tree_addr.len() > 0 { // create editor - let mut e = Context::make_node(&self.ctx, t.0[0].clone(), *ed_depth+1).unwrap(); + let mut e = Context::make_node(&self.ctx, t.clone(), *ed_depth+1).unwrap(); *editor = Some(e.clone()); e.goto(c.clone()); } @@ -128,7 +128,7 @@ impl TreeNav for ProductEditor { } else { // create editor - let mut e = Context::make_node(&self.ctx, t.0[0].clone(), *ed_depth+1).unwrap(); + let mut e = Context::make_node(&self.ctx, t.clone(), *ed_depth+1).unwrap(); *editor = Some(e.clone()); e.goby(direction); } diff --git a/nested/src/editors/product/segment.rs b/nested/src/editors/product/segment.rs index 238d330..0e20cb9 100644 --- a/nested/src/editors/product/segment.rs +++ b/nested/src/editors/product/segment.rs @@ -5,7 +5,7 @@ use { } }, crate::{ - type_system::{TypeLadder, Context}, + type_system::{Context, TypeTerm}, terminal::{ TerminalStyle, TerminalView, make_label @@ -20,7 +20,7 @@ use { pub enum ProductEditorSegment { T( String, usize ), N { - t: TypeLadder, + t: TypeTerm, editor: Option, ed_depth: usize, cur_depth: usize, @@ -65,7 +65,7 @@ impl ProductEditorSegment { }), ProductEditorSegment::N{ t, editor: None, ed_depth, cur_depth, cur_dist } => - make_label(&ctx.read().unwrap().type_term_to_str(&t.0[0])) + make_label(&ctx.read().unwrap().type_term_to_str(t)) .map_item({ let _cur_depth = *cur_depth; let _ed_depth = *ed_depth; diff --git a/nested/src/tree/treetype.rs b/nested/src/tree/treetype.rs index 79760dd..9fd9ae3 100644 --- a/nested/src/tree/treetype.rs +++ b/nested/src/tree/treetype.rs @@ -1,14 +1,14 @@ use { crate::{ - type_system::TypeLadder, + type_system::{TypeTerm, TypeID}, tree::{TreeAddr} } }; pub trait TreeType { - fn get_type(&self, _addr: &TreeAddr) -> TypeLadder { - vec![].into() + fn get_type(&self, _addr: &TreeAddr) -> TypeTerm { + TypeTerm::new(TypeID::Var(0)) } } diff --git a/nested/src/type_system/context.rs b/nested/src/type_system/context.rs index 0f57836..169ac18 100644 --- a/nested/src/type_system/context.rs +++ b/nested/src/type_system/context.rs @@ -1,6 +1,6 @@ use { crate::{ - type_system::{TypeDict, TypeTerm, TypeID, ReprTree, TypeLadder}, + type_system::{TypeDict, TypeTerm, TypeID, ReprTree}, tree::NestedNode }, std::{ @@ -44,18 +44,24 @@ pub struct MorphismTypePattern { pub dst_tyid: TypeID } -impl From for MorphismTypePattern { +impl From for MorphismTypePattern { fn from(value: MorphismType) -> MorphismTypePattern { + fn strip( x: &TypeTerm ) -> TypeID { + match x { + TypeTerm::TypeID(id) => id.clone(), + TypeTerm::App(args) => strip(&args[0]), + TypeTerm::Ladder(args) => strip(&args[0]), + _ => unreachable!() + } + } + MorphismTypePattern { src_tyid: match value.src_type { - Some(TypeTerm::Type { id, args: _ }) => Some(TypeID::Fun(id)), + Some(TypeTerm::TypeID(id)) => Some(id), _ => None, }, - dst_tyid: match value.dst_type { - TypeTerm::Type { id, args: _ } => TypeID::Fun(id), - _ => unreachable!() - } + dst_tyid: strip(&value.dst_type) } } } @@ -138,8 +144,8 @@ impl Context { pub fn is_list_type(&self, t: &TypeTerm) -> bool { match t { - TypeTerm::Type { id, args: _ } => { - self.list_types.contains(&TypeID::Fun(*id)) + TypeTerm::TypeID(id) => { + self.list_types.contains(id) } _ => false } @@ -156,6 +162,10 @@ impl Context { } } + pub fn get_typename(&self, tid: &TypeID) -> Option { + self.type_dict.read().unwrap().get_typename(tid) + } + pub fn get_var_typeid(&self, tn: &str) -> Option { match self.get_typeid(tn) { Some(TypeID::Var(x)) => Some(x), @@ -219,7 +229,7 @@ impl Context { let mk_node = ctx.read().unwrap().get_morphism(MorphismType { src_type: None, dst_type: type_term.clone() - })?; + }).expect("morphism"); mk_node(NestedNode::new(depth).set_ctx( Arc::new(RwLock::new( diff --git a/nested/src/type_system/dict.rs b/nested/src/type_system/dict.rs index 7ef52f6..1832af2 100644 --- a/nested/src/type_system/dict.rs +++ b/nested/src/type_system/dict.rs @@ -1,7 +1,7 @@ use { crate::{ utils::Bimap, - type_system::{TypeTerm, TypeLadder} + type_system::{TypeTerm} } }; @@ -61,10 +61,6 @@ impl TypeDict { pub fn type_term_to_str(&self, term: &TypeTerm) -> String { term.to_str(&self.typenames.my) } - - pub fn type_ladder_to_str(&self, ladder: &TypeLadder) -> String { - ladder.to_str1(&self.typenames.my) - } } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> diff --git a/nested/src/type_system/editor.rs b/nested/src/type_system/editor.rs index 90fac88..32b21cb 100644 --- a/nested/src/type_system/editor.rs +++ b/nested/src/type_system/editor.rs @@ -6,7 +6,7 @@ use { projection::flatten_singleton::* }, crate::{ - type_system::{Context, TypeTerm, ReprTree, MorphismTypePattern}, + type_system::{Context, TypeID, TypeTerm, ReprTree, MorphismTypePattern}, terminal::{TerminalEvent}, editors::{sum::*, list::{ListCursorMode, ListEditor, PTYListStyle, PTYListController}}, tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor}, @@ -32,6 +32,7 @@ enum State { pub struct TypeTermEditor { ctx: Arc>, + data: Arc>, editor: SingletonBuffer< Option< Arc > >, @@ -43,6 +44,9 @@ pub struct TypeTermEditor { impl TypeTermEditor { pub fn init_ctx(ctx: &mut Context) { ctx.add_list_typename("TypeTerm".into()); + ctx.add_list_typename("TypeSymbol".into()); + ctx.add_list_typename("TypeSymbol::Function".into()); + ctx.add_list_typename("TypeSymbol::Variable".into()); ctx.add_node_ctor( "TypeTerm", Arc::new( |ctx: Arc>, _ty: TypeTerm, depth: usize| { @@ -98,6 +102,17 @@ impl TypeTermEditor { grid.get_port() .flatten() ); + + self.data.write().unwrap().insert_leaf( + vec![].into_iter(), + node.data.clone().unwrap().read().unwrap() + .get_port::>().unwrap() + .map( + |c| TypeTerm::Char(c) + ) + .into() + ); + node } State::List => { @@ -106,6 +121,18 @@ impl TypeTermEditor { PTYListController::for_node( &mut node, Some(' '), Some('>') ); PTYListStyle::for_node( &mut node, ("<"," ",">") ); + self.data.write().unwrap().insert_leaf( + vec![].into_iter(), + node.data.clone().unwrap().read().unwrap() + .get_port::>().unwrap() + .map( + |node| { + node.data.as_ref().unwrap().read().unwrap().get_port::>().unwrap() + } + ) + .into() + ); + node } State::Symbol => { @@ -131,9 +158,16 @@ impl TypeTermEditor { } fn with_node(ctx: Arc>, depth: usize, node: NestedNode, state: State) -> NestedNode { + let buffer = SingletonBuffer::>::new( None ); + + let data = Arc::new(RwLock::new(ReprTree::new( + (&ctx, "( TypeTerm )") + ))); + let mut editor = TypeTermEditor { ctx: ctx.clone(), state, + data: data.clone(), cur_node: SingletonBuffer::new(node), editor: SingletonBuffer::new(None) }; @@ -161,14 +195,54 @@ impl TypeTermEditor { let mut node = NestedNode::new(depth) .set_ctx(ctx) .set_view(view) + .set_data(data) .set_nav(editor.clone()) .set_cmd(editor.clone()) .set_editor(editor.clone()); + node.close_char.set(cc.get()); editor.write().unwrap().editor = node.editor.clone(); node } + + fn get_typeterm(&self) -> Option { + match self.state { + State::Any => None, + + State::Symbol => { + /* + let x = self.data.descend_ladder(vec![ + (&ctx, "( FunctionID )").into(), + (&ctx, "( Symbol )").into(), + (&ctx, "( List Char )").into(), + ].into_iter()); + + let fun_name = /* x...*/ "PosInt"; + let fun_id = self.ctx.read().unwrap().get_typeid( fun_name ); + + self.data.add_repr( + vec![ + (&ctx, "( FunctionID )").into(), + (&ctx, "( MachineInt )").into() + ] + ); +*/ + Some(TypeTerm::new(TypeID::Fun(0))) + }, + State::List => { + Some(TypeTerm::new(TypeID::Fun(0))) + }, + + State::Char => { + Some(TypeTerm::Char('c')) + } + State::Num => { + Some(TypeTerm::Num(44)) + } + _ => {None} + } + } } impl TreeNav for TypeTermEditor { @@ -252,6 +326,8 @@ impl ObjCommander for TypeTermEditor { } State::List => { + self.cur_node.get_mut().send_cmd_obj( co ) + /* match self.cur_node.get_mut().send_cmd_obj( co ) { TreeNavResult::Continue => { TreeNavResult::Continue @@ -277,9 +353,10 @@ impl ObjCommander for TypeTermEditor { _ => { TreeNavResult::Exit } - } } - } + } + } + */ } _ => { @@ -290,7 +367,17 @@ impl ObjCommander for TypeTermEditor { TreeNavResult::Exit } } else { - self.cur_node.get_mut().send_cmd_obj( co ) +// eprintln!("undefined comd object"); + match &self.state { + State::Any => { + eprintln!("undefined comd object set to listl"); + self.set_state( State::List ); + self.cur_node.get_mut().goto(TreeCursor::home()); + } + _ => {} + } + + self.cur_node.get().cmd.get().unwrap().write().unwrap().send_cmd_obj( co ) } } } diff --git a/nested/src/type_system/ladder.rs b/nested/src/type_system/ladder.rs index d730452..ca7fef0 100644 --- a/nested/src/type_system/ladder.rs +++ b/nested/src/type_system/ladder.rs @@ -61,7 +61,7 @@ impl TypeLadder { s = s + "~"; } first = false; - s = s + &t.to_str1(names); + s = s + &t.to_str(names); } s } diff --git a/nested/src/type_system/make_editor.rs b/nested/src/type_system/make_editor.rs index f340e80..8dcec4e 100644 --- a/nested/src/type_system/make_editor.rs +++ b/nested/src/type_system/make_editor.rs @@ -22,10 +22,8 @@ pub fn init_mem_ctx(parent: Arc>) -> Arc> { "Vec", Arc::new( |ctx: Arc>, ty: TypeTerm, depth: usize| { match ty { - TypeTerm::Type { - id: _, args - } => { - if args.len() > 0 { + TypeTerm::App(args) => { + if args.len() > 1 { let buf = r3vi::buffer::vec::VecBuffer::::new(); let data = ReprTree::new_leaf( ctx.read().unwrap().type_term_from_str("( Char )").unwrap(), @@ -52,9 +50,12 @@ pub fn init_mem_ctx(parent: Arc>) -> Arc> { } pub fn init_editor_ctx(parent: Arc>) -> Arc> { - let ctx = Arc::new(RwLock::new(Context::with_parent(Some(parent)))); + let ctx0 = Arc::new(RwLock::new(Context::with_parent(Some(parent)))); + ListEditor::init_ctx( &ctx0 ); - ctx.write().unwrap().add_node_ctor( + let mut ctx = ctx0.write().unwrap(); + + ctx.add_node_ctor( "Char", Arc::new( |ctx: Arc>, _ty: TypeTerm, _depth: usize| { Some(CharEditor::new_node(ctx)) @@ -62,50 +63,51 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { ) ); - ctx.write().unwrap().add_list_typename("Seq".into()); - ctx.write().unwrap().add_list_typename("Sequence".into()); - ctx.write().unwrap().add_list_typename("SepSeq".into()); - ctx.write().unwrap().add_typename("NestedNode".into()); - ListEditor::init_ctx( &ctx ); + ctx.add_list_typename("Seq".into()); + ctx.add_list_typename("Sequence".into()); + ctx.add_list_typename("SepSeq".into()); + ctx.add_typename("NestedNode".into()); - ctx.write().unwrap().add_list_typename("Symbol".into()); + + ctx.add_list_typename("Symbol".into()); let pattern = MorphismTypePattern { - src_tyid: ctx.read().unwrap().get_typeid("List"), - dst_tyid: ctx.read().unwrap().get_typeid("Symbol").unwrap() + src_tyid: ctx.get_typeid("List"), + dst_tyid: ctx.get_typeid("Symbol").unwrap() }; - ctx.write().unwrap().add_morphism(pattern, + ctx.add_morphism(pattern, Arc::new( |mut node, _dst_type:_| { PTYListController::for_node( &mut node, None, None ); PTYListStyle::for_node( &mut node, ("","","") ); + Some(node) } ) ); - ctx.write().unwrap().add_node_ctor( + ctx.add_node_ctor( "Symbol", Arc::new( |ctx: Arc>, dst_typ: TypeTerm, depth: usize| { let mut node = Context::make_node( &ctx, (&ctx, "( List Char )").into(), depth+1 - ).unwrap(); + ).expect("nested node"); - node = node.morph(dst_typ); + //node = node.morph(dst_typ); Some(node) } ) ); - ctx.write().unwrap().add_list_typename("String".into()); + ctx.add_list_typename("String".into()); let pattern = MorphismTypePattern { - src_tyid: ctx.read().unwrap().get_typeid("List"), - dst_tyid: ctx.read().unwrap().get_typeid("String").unwrap() + src_tyid: ctx.get_typeid("List"), + dst_tyid: ctx.get_typeid("String").unwrap() }; - ctx.write().unwrap().add_morphism(pattern, + ctx.add_morphism(pattern, Arc::new( |mut node, _dst_type:_| { PTYListController::for_node( &mut node, None, Some('\"') ); @@ -115,17 +117,15 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { ) ); - ctx.write().unwrap().add_node_ctor( + ctx.add_node_ctor( "String", Arc::new( |ctx: Arc>, dst_typ: TypeTerm, depth: usize| { let mut node = Context::make_node( &ctx, - TypeTerm::Type { - id: ctx.read().unwrap().get_fun_typeid("List").unwrap(), - args: vec![ - TypeTerm::new(ctx.read().unwrap().get_typeid("Char").unwrap()).into() - ] - }, + TypeTerm::App(vec![ + TypeTerm::TypeID(ctx.read().unwrap().get_typeid("List").unwrap()), + TypeTerm::new(ctx.read().unwrap().get_typeid("Char").unwrap()) + ]), depth+1 ).unwrap(); @@ -136,8 +136,8 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { ) ); /* - ctx.write().unwrap().add_list_typename("TypeTerm".into()); - ctx.write().unwrap().add_node_ctor( + ctx.add_list_typename("TypeTerm".into()); + ctx.add_node_ctor( "TypeTerm", Arc::new( |ctx: Arc>, _ty: TypeTerm, depth: usize| { Some(TypeTermEditor::new(ctx, depth).into_node(depth)) @@ -145,27 +145,29 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { ) ); */ - ctx.write().unwrap().add_typename("TerminalEvent".into()); - ctx + ctx.add_typename("TerminalEvent".into()); + + drop(ctx); + ctx0 } pub fn init_math_ctx(parent: Arc>) -> Arc> { - let ctx = Arc::new(RwLock::new(Context::with_parent(Some(parent)))); + let ctx0 = Arc::new(RwLock::new(Context::with_parent(Some(parent)))); - ctx.write().unwrap().add_typename("MachineInt".into()); - ctx.write().unwrap().add_typename("u32".into()); - ctx.write().unwrap().add_typename("LittleEndian".into()); - ctx.write().unwrap().add_typename("BigEndian".into()); + let mut ctx = ctx0.write().unwrap(); + ctx.add_typename("MachineInt".into()); + ctx.add_typename("u32".into()); + ctx.add_typename("u64".into()); + ctx.add_typename("LittleEndian".into()); + ctx.add_typename("BigEndian".into()); - ctx.write().unwrap().add_node_ctor( + ctx.add_node_ctor( "Digit", Arc::new( |ctx: Arc>, ty: TypeTerm, depth: usize| { match ty { - TypeTerm::Type { - id: _, args - } => { - if args.len() > 0 { - match (args[0].0)[0] { + TypeTerm::App(args) => { + if args.len() > 1 { + match args[1] { TypeTerm::Num(radix) => { let node = DigitEditor::new(ctx.clone(), radix as u32).into_node(depth); Some( @@ -184,25 +186,23 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { ) ); - ctx.write().unwrap().add_list_typename("PosInt".into()); + ctx.add_list_typename("PosInt".into()); let pattern = MorphismTypePattern { - src_tyid: ctx.read().unwrap().get_typeid("List"), - dst_tyid: ctx.read().unwrap().get_typeid("PosInt").unwrap() + src_tyid: ctx.get_typeid("List"), + dst_tyid: ctx.get_typeid("PosInt").unwrap() }; - ctx.write().unwrap().add_morphism(pattern, + ctx.add_morphism(pattern, Arc::new( |mut node, dst_type| { let depth = node.depth.get(); let editor = node.editor.get().unwrap().downcast::>().unwrap(); // todo: check src_type parameter to be ( Digit radix ) - + match dst_type { - TypeTerm::Type { - id: _, args - } => { - if args.len() > 0 { - match (args[0].0)[0] { + TypeTerm::App(args) => { + if args.len() > 1 { + match args[1] { TypeTerm::Num(_radix) => { PTYListController::for_node( &mut node, @@ -229,28 +229,26 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { ) ); - ctx.write().unwrap().add_node_ctor( + ctx.add_node_ctor( "PosInt", Arc::new( - |ctx: Arc>, dst_typ: TypeTerm, depth: usize| { + |ctx0: Arc>, dst_typ: TypeTerm, depth: usize| { match dst_typ.clone() { - TypeTerm::Type { - id: _, args - } => { - if args.len() > 0 { - match (args[0].0)[0] { + TypeTerm::App(args) => { + if args.len() > 1 { + match args[1] { TypeTerm::Num(radix) => { - + let ctx = ctx0.read().unwrap(); let mut node = Context::make_node( - &ctx, - TypeTerm::Type { - id: ctx.read().unwrap().get_fun_typeid("List").unwrap(), - args: vec![ - TypeTerm::new(ctx.read().unwrap().get_typeid("Digit").unwrap()) - .num_arg(radix) - .clone() - .into() - ] - }, + &ctx0, + TypeTerm::App(vec![ + TypeTerm::TypeID(ctx.get_typeid("List").unwrap()), + TypeTerm::TypeID( + ctx.get_typeid("Digit").unwrap() + ) + .num_arg(radix) + .clone() + .into() + ]), depth+1 ).unwrap(); @@ -269,52 +267,15 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { } ) ); - - ctx.write().unwrap().add_list_typename("RGB".into()); - ctx.write().unwrap().add_node_ctor( - "RGB", Arc::new( - |ctx: Arc>, _ty: TypeTerm, depth: usize| { - let editor = ProductEditor::new(depth, ctx.clone()) - .with_t(Point2::new(0, 0), "r: ") - .with_n(Point2::new(1, 0), - vec![ - ctx.read().unwrap().type_term_from_str("( PosInt 16 BigEndian )").unwrap() - ].into()) - .with_t(Point2::new(0, 1), "g: ") - .with_n(Point2::new(1, 1), - vec![ - ctx.read().unwrap().type_term_from_str("( PosInt 16 BigEndian )").unwrap() - ].into()) - .with_t(Point2::new(0, 2), "b: ") - .with_n(Point2::new(1, 2), - vec![ - ctx.read().unwrap().type_term_from_str("( PosInt 16 BigEndian )").unwrap() - ].into() - ); - - let view = editor.get_term_view(); - let diag = editor.get_msg_port(); - let editor = Arc::new(RwLock::new(editor)); - - let node = NestedNode::new(depth) - .set_ctx(ctx) - .set_cmd(editor.clone()) - .set_nav(editor.clone()) - .set_view(view) - .set_diag(diag) - ; - - Some(node) - } - )); - - ctx.write().unwrap().add_typename("Date".into()); - ctx.write().unwrap().add_typename("ISO-8601".into()); - ctx.write().unwrap().add_typename("TimeSinceEpoch".into()); - ctx.write().unwrap().add_typename("Duration".into()); - ctx.write().unwrap().add_typename("Seconds".into()); - ctx.write().unwrap().add_typename("ℕ".into()); - ctx + ctx.add_typename("Date".into()); + ctx.add_typename("ISO-8601".into()); + ctx.add_typename("TimeSinceEpoch".into()); + ctx.add_typename("Duration".into()); + ctx.add_typename("Seconds".into()); + ctx.add_typename("ℕ".into()); + + drop(ctx); + ctx0 } diff --git a/nested/src/type_system/mod.rs b/nested/src/type_system/mod.rs index 3ed099f..2bfde44 100644 --- a/nested/src/type_system/mod.rs +++ b/nested/src/type_system/mod.rs @@ -2,14 +2,14 @@ pub mod context; pub mod dict; pub mod term; -pub mod ladder; +//pub mod ladder; pub mod repr_tree; pub mod make_editor; pub mod editor; pub use { dict::*, - ladder::*, +// ladder::*, repr_tree::*, term::*, context::{Context, MorphismMode, MorphismType, MorphismTypePattern}, diff --git a/nested/src/type_system/repr_tree.rs b/nested/src/type_system/repr_tree.rs index 52e8d32..87164f3 100644 --- a/nested/src/type_system/repr_tree.rs +++ b/nested/src/type_system/repr_tree.rs @@ -89,8 +89,7 @@ impl ReprTree { self.port .clone()? .downcast::() - .ok() - .unwrap() + .ok()? ) } diff --git a/nested/src/type_system/term.rs b/nested/src/type_system/term.rs index 3dedfdf..9fad7d7 100644 --- a/nested/src/type_system/term.rs +++ b/nested/src/type_system/term.rs @@ -1,43 +1,54 @@ use { crate::{ - type_system::{TypeLadder, TypeID} + type_system::{TypeID} }, std::collections::HashMap }; //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + #[derive(Clone, PartialEq, Eq, Hash, Debug)] pub enum TypeTerm { - /* TODO: refactor into this: - Nominal { - id: u64, - args: Vec< TypeTerm > - }, - Ladder(Vec< TypeTerm >), - */ - Type { - id: u64, - args: Vec< TypeLadder > - }, - Var(u64), + /* Atomic Terms */ + + // Base types from dictionary + TypeID(TypeID), + + // Literals Num(i64), - Char(char) + Char(char), + + + /* Complex Terms */ + + // Type Parameters + // avoid currying to save space & indirection + App(Vec< TypeTerm >), + + // Type Ladders + Ladder(Vec< TypeTerm >), } //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> impl TypeTerm { pub fn new(id: TypeID) -> Self { - match id { - TypeID::Fun(id) => TypeTerm::Type { id, args: vec![] }, - TypeID::Var(_) => {unreachable!();} - } + TypeTerm::TypeID(id) } - pub fn arg(&mut self, t: impl Into) -> &mut Self { - if let TypeTerm::Type { id: _, args } = self { - args.push(t.into()); + 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 @@ -51,6 +62,29 @@ impl TypeTerm { self.arg(TypeTerm::Char(c)) } + /* TODO + + // summarize all curried applications into one vec + pub fn decurry() {} + + // transmute into Ladder-Normal-Form + pub fn normalize(&mut self) { + match self { + TypeTerm::Apply{ id, args } => { + + } + } + } + + pub fn is_supertype_of(&self, t: &TypeTerm) -> bool { + t.is_subtype_of(self) + } + + pub fn is_subtype_of(&self, t: &TypeTerm) -> bool { + false + } + */ + pub fn from_str(s: &str, names: &HashMap) -> Option { let mut term_stack = Vec::>::new(); @@ -111,53 +145,42 @@ impl TypeTerm { None } - // only adds parenthesis where args.len > 0 - pub fn to_str1(&self, names: &HashMap) -> String { + pub fn to_str(&self, names: &HashMap) -> String { match self { - TypeTerm::Type { id, args } => { - if args.len() > 0 { - format!( - "<{}{}>", - names[&TypeID::Fun(*id)], - if args.len() > 0 { - args.iter().fold(String::new(), |str, term| { - format!("{} {}", str, term.to_str1(names)) - }) - } else { - String::new() - } - ) - } else { - names[&TypeID::Fun(*id)].clone() + TypeTerm::App(args) => { + let mut out = String::new(); + + out.push_str(&"<"); + + for x in args.iter() { + out.push_str(&" "); + 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(&"~"); + 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::Var(varid) => format!("T"), - } - } - - // always adds an enclosing pair of parenthesis - pub fn to_str(&self, names: &HashMap) -> String { - match self { - TypeTerm::Type { id, args } => format!( - "<{}{}>", - names[&TypeID::Fun(*id)], - if args.len() > 0 { - args.iter().fold(String::new(), |str, term| { - format!("{} {}", str, term.to_str1(names)) - }) - } else { - String::new() - } - ), - - TypeTerm::Num(n) => format!("{}", n), - TypeTerm::Char('\n') => format!("'\\n'"), - TypeTerm::Char(c) => format!("'{}'", c), - TypeTerm::Var(varid) => format!("T"), + TypeTerm::TypeID(id) => format!("{}", names[id]), } } }