restructure TypeTerm
This commit is contained in:
parent
64dc82dfbb
commit
2d46ac95bd
15 changed files with 312 additions and 242 deletions
|
@ -117,12 +117,7 @@ impl DigitEditor {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_type(&self) -> TypeTerm {
|
pub fn get_type(&self) -> TypeTerm {
|
||||||
TypeTerm::Type {
|
TypeTerm::TypeID(self.ctx.read().unwrap().get_typeid("Digit").unwrap())
|
||||||
id: self.ctx.read().unwrap().get_fun_typeid("Digit").unwrap(),
|
|
||||||
args: vec![
|
|
||||||
TypeTerm::Num(self.radix as i64).into()
|
|
||||||
]
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_data(&self) -> Arc<RwLock<ReprTree>> {
|
pub fn get_data(&self) -> Arc<RwLock<ReprTree>> {
|
||||||
|
@ -163,17 +158,12 @@ impl PosIntEditor {
|
||||||
let data = node.data.clone().unwrap();
|
let data = node.data.clone().unwrap();
|
||||||
node = node.set_data(ReprTree::ascend(
|
node = node.set_data(ReprTree::ascend(
|
||||||
&data,
|
&data,
|
||||||
TypeTerm::Type {
|
TypeTerm::App(vec![
|
||||||
id: ctx.read().unwrap().get_fun_typeid("PosInt").unwrap(),
|
TypeTerm::TypeID(ctx.read().unwrap().get_typeid("PosInt").unwrap()),
|
||||||
args: vec![
|
TypeTerm::Num(radix as i64).into(),
|
||||||
TypeTerm::Num(radix as i64).into(),
|
TypeTerm::TypeID(ctx.read().unwrap().get_typeid("BigEndian").unwrap())
|
||||||
TypeTerm::Type {
|
|
||||||
id: ctx.read().unwrap().get_fun_typeid("BigEndian").unwrap(),
|
|
||||||
args: vec![]
|
|
||||||
}.into()
|
|
||||||
]
|
]
|
||||||
}
|
)));
|
||||||
));
|
|
||||||
|
|
||||||
PosIntEditor {
|
PosIntEditor {
|
||||||
radix,
|
radix,
|
||||||
|
|
|
@ -32,7 +32,13 @@ impl ListCmd {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
/*
|
||||||
|
impl Into< Arc<RwLock<ReprTree>> > for (&Arc<RwLock<Context>>, ListCmd) {
|
||||||
|
fn into(self) -> Arc<RwLock<ReprTree>> {
|
||||||
|
self.1.into_repr_tree(self.0)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
*/
|
||||||
impl ObjCommander for ListEditor {
|
impl ObjCommander for ListEditor {
|
||||||
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 cmd_repr = cmd_obj.read().unwrap();
|
let cmd_repr = cmd_obj.read().unwrap();
|
||||||
|
|
|
@ -38,11 +38,9 @@ impl ListEditor {
|
||||||
"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 {
|
||||||
TypeTerm::Type {
|
TypeTerm::App(args) => {
|
||||||
id: _, args
|
if args.len() > 1 {
|
||||||
} => {
|
let typ = args[1].clone();
|
||||||
if args.len() > 0 {
|
|
||||||
let typ = (args[0].clone().0)[0].clone();
|
|
||||||
|
|
||||||
let mut node = ListEditor::new(ctx.clone(), typ).into_node(depth);
|
let mut node = ListEditor::new(ctx.clone(), typ).into_node(depth);
|
||||||
|
|
||||||
|
@ -160,10 +158,10 @@ impl ListEditor {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_seq_type(&self) -> TypeTerm {
|
pub fn get_seq_type(&self) -> TypeTerm {
|
||||||
TypeTerm::Type {
|
TypeTerm::App(vec![
|
||||||
id: self.ctx.read().unwrap().get_fun_typeid("List").unwrap(),
|
TypeTerm::TypeID(self.ctx.read().unwrap().get_typeid("List").unwrap()),
|
||||||
args: vec![ self.get_item_type().into() ]
|
self.get_item_type().into()
|
||||||
}
|
])
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn get_cursor_port(&self) -> OuterViewPort<dyn SingletonView<Item = ListCursor>> {
|
pub fn get_cursor_port(&self) -> OuterViewPort<dyn SingletonView<Item = ListCursor>> {
|
||||||
|
|
|
@ -10,7 +10,7 @@ use {
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeLadder, Context},
|
type_system::{Context, TypeTerm},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalEditor, TerminalEditorResult,
|
TerminalEditor, TerminalEditorResult,
|
||||||
TerminalEvent, TerminalView
|
TerminalEvent, TerminalView
|
||||||
|
@ -79,7 +79,7 @@ impl ProductEditor {
|
||||||
self
|
self
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn with_n(mut self, pos: Point2<i16>, n: TypeLadder) -> Self {
|
pub fn with_n(mut self, pos: Point2<i16>, n: &TypeTerm) -> Self {
|
||||||
self.segments.insert(pos, ProductEditorSegment::N{
|
self.segments.insert(pos, ProductEditorSegment::N{
|
||||||
t: n.clone(),
|
t: n.clone(),
|
||||||
editor: None,
|
editor: None,
|
||||||
|
@ -90,7 +90,7 @@ impl ProductEditor {
|
||||||
self.n_indices.push(pos);
|
self.n_indices.push(pos);
|
||||||
|
|
||||||
let mut b = VecBuffer::new();
|
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.msg_buf.push(Some(b.get_port().to_sequence()));
|
||||||
self
|
self
|
||||||
}
|
}
|
||||||
|
@ -157,7 +157,7 @@ impl ProductEditor {
|
||||||
self.msg_buf.update(idx as usize, Some(e.get_msg_port()));
|
self.msg_buf.update(idx as usize, Some(e.get_msg_port()));
|
||||||
} else {
|
} else {
|
||||||
let mut b = VecBuffer::new();
|
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()));
|
self.msg_buf.update(idx as usize, Some(b.get_port().to_sequence()));
|
||||||
|
|
||||||
|
@ -238,7 +238,7 @@ impl ObjCommander for ProductEditor {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
} else {
|
} 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());
|
*editor = Some(e.clone());
|
||||||
update_segment = true;
|
update_segment = true;
|
||||||
|
|
||||||
|
|
|
@ -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_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());
|
*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_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());
|
*editor = Some(e.clone());
|
||||||
e.goby(direction);
|
e.goby(direction);
|
||||||
}
|
}
|
||||||
|
|
|
@ -5,7 +5,7 @@ use {
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeLadder, Context},
|
type_system::{Context, TypeTerm},
|
||||||
terminal::{
|
terminal::{
|
||||||
TerminalStyle, TerminalView,
|
TerminalStyle, TerminalView,
|
||||||
make_label
|
make_label
|
||||||
|
@ -20,7 +20,7 @@ use {
|
||||||
pub enum ProductEditorSegment {
|
pub enum ProductEditorSegment {
|
||||||
T( String, usize ),
|
T( String, usize ),
|
||||||
N {
|
N {
|
||||||
t: TypeLadder,
|
t: TypeTerm,
|
||||||
editor: Option<NestedNode>,
|
editor: Option<NestedNode>,
|
||||||
ed_depth: usize,
|
ed_depth: usize,
|
||||||
cur_depth: usize,
|
cur_depth: usize,
|
||||||
|
@ -65,7 +65,7 @@ impl ProductEditorSegment {
|
||||||
}),
|
}),
|
||||||
|
|
||||||
ProductEditorSegment::N{ t, editor: None, ed_depth, cur_depth, cur_dist } =>
|
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({
|
.map_item({
|
||||||
let _cur_depth = *cur_depth;
|
let _cur_depth = *cur_depth;
|
||||||
let _ed_depth = *ed_depth;
|
let _ed_depth = *ed_depth;
|
||||||
|
|
|
@ -1,14 +1,14 @@
|
||||||
|
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
type_system::TypeLadder,
|
type_system::{TypeTerm, TypeID},
|
||||||
tree::{TreeAddr}
|
tree::{TreeAddr}
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
pub trait TreeType {
|
pub trait TreeType {
|
||||||
fn get_type(&self, _addr: &TreeAddr) -> TypeLadder {
|
fn get_type(&self, _addr: &TreeAddr) -> TypeTerm {
|
||||||
vec![].into()
|
TypeTerm::new(TypeID::Var(0))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeDict, TypeTerm, TypeID, ReprTree, TypeLadder},
|
type_system::{TypeDict, TypeTerm, TypeID, ReprTree},
|
||||||
tree::NestedNode
|
tree::NestedNode
|
||||||
},
|
},
|
||||||
std::{
|
std::{
|
||||||
|
@ -44,18 +44,24 @@ pub struct MorphismTypePattern {
|
||||||
pub dst_tyid: TypeID
|
pub dst_tyid: TypeID
|
||||||
}
|
}
|
||||||
|
|
||||||
impl From<MorphismType> for MorphismTypePattern {
|
impl From<MorphismType> for MorphismTypePattern {
|
||||||
fn from(value: MorphismType) -> 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 {
|
MorphismTypePattern {
|
||||||
src_tyid: match value.src_type {
|
src_tyid: match value.src_type {
|
||||||
Some(TypeTerm::Type { id, args: _ }) => Some(TypeID::Fun(id)),
|
Some(TypeTerm::TypeID(id)) => Some(id),
|
||||||
_ => None,
|
_ => None,
|
||||||
},
|
},
|
||||||
|
|
||||||
dst_tyid: match value.dst_type {
|
dst_tyid: strip(&value.dst_type)
|
||||||
TypeTerm::Type { id, args: _ } => TypeID::Fun(id),
|
|
||||||
_ => unreachable!()
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -138,8 +144,8 @@ impl Context {
|
||||||
|
|
||||||
pub fn is_list_type(&self, t: &TypeTerm) -> bool {
|
pub fn is_list_type(&self, t: &TypeTerm) -> bool {
|
||||||
match t {
|
match t {
|
||||||
TypeTerm::Type { id, args: _ } => {
|
TypeTerm::TypeID(id) => {
|
||||||
self.list_types.contains(&TypeID::Fun(*id))
|
self.list_types.contains(id)
|
||||||
}
|
}
|
||||||
_ => false
|
_ => false
|
||||||
}
|
}
|
||||||
|
@ -156,6 +162,10 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn get_typename(&self, tid: &TypeID) -> Option<String> {
|
||||||
|
self.type_dict.read().unwrap().get_typename(tid)
|
||||||
|
}
|
||||||
|
|
||||||
pub fn get_var_typeid(&self, tn: &str) -> Option<u64> {
|
pub fn get_var_typeid(&self, tn: &str) -> Option<u64> {
|
||||||
match self.get_typeid(tn) {
|
match self.get_typeid(tn) {
|
||||||
Some(TypeID::Var(x)) => Some(x),
|
Some(TypeID::Var(x)) => Some(x),
|
||||||
|
@ -219,7 +229,7 @@ impl Context {
|
||||||
let mk_node = ctx.read().unwrap().get_morphism(MorphismType {
|
let mk_node = ctx.read().unwrap().get_morphism(MorphismType {
|
||||||
src_type: None,
|
src_type: None,
|
||||||
dst_type: type_term.clone()
|
dst_type: type_term.clone()
|
||||||
})?;
|
}).expect("morphism");
|
||||||
|
|
||||||
mk_node(NestedNode::new(depth).set_ctx(
|
mk_node(NestedNode::new(depth).set_ctx(
|
||||||
Arc::new(RwLock::new(
|
Arc::new(RwLock::new(
|
||||||
|
|
|
@ -1,7 +1,7 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
utils::Bimap,
|
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 {
|
pub fn type_term_to_str(&self, term: &TypeTerm) -> String {
|
||||||
term.to_str(&self.typenames.my)
|
term.to_str(&self.typenames.my)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn type_ladder_to_str(&self, ladder: &TypeLadder) -> String {
|
|
||||||
ladder.to_str1(&self.typenames.my)
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
|
@ -6,7 +6,7 @@ use {
|
||||||
projection::flatten_singleton::*
|
projection::flatten_singleton::*
|
||||||
},
|
},
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{Context, TypeTerm, ReprTree, MorphismTypePattern},
|
type_system::{Context, TypeID, TypeTerm, ReprTree, MorphismTypePattern},
|
||||||
terminal::{TerminalEvent},
|
terminal::{TerminalEvent},
|
||||||
editors::{sum::*, list::{ListCursorMode, ListEditor, PTYListStyle, PTYListController}},
|
editors::{sum::*, list::{ListCursorMode, ListEditor, PTYListStyle, PTYListController}},
|
||||||
tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor},
|
tree::{NestedNode, TreeNav, TreeNavResult, TreeCursor},
|
||||||
|
@ -32,6 +32,7 @@ enum State {
|
||||||
pub struct TypeTermEditor {
|
pub struct TypeTermEditor {
|
||||||
ctx: Arc<RwLock<Context>>,
|
ctx: Arc<RwLock<Context>>,
|
||||||
|
|
||||||
|
data: Arc<RwLock<ReprTree>>,
|
||||||
editor: SingletonBuffer<
|
editor: SingletonBuffer<
|
||||||
Option< Arc<dyn Any + Send + Sync> >
|
Option< Arc<dyn Any + Send + Sync> >
|
||||||
>,
|
>,
|
||||||
|
@ -43,6 +44,9 @@ pub struct TypeTermEditor {
|
||||||
impl TypeTermEditor {
|
impl TypeTermEditor {
|
||||||
pub fn init_ctx(ctx: &mut Context) {
|
pub fn init_ctx(ctx: &mut Context) {
|
||||||
ctx.add_list_typename("TypeTerm".into());
|
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(
|
ctx.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| {
|
||||||
|
@ -98,6 +102,17 @@ impl TypeTermEditor {
|
||||||
grid.get_port()
|
grid.get_port()
|
||||||
.flatten()
|
.flatten()
|
||||||
);
|
);
|
||||||
|
|
||||||
|
self.data.write().unwrap().insert_leaf(
|
||||||
|
vec![].into_iter(),
|
||||||
|
node.data.clone().unwrap().read().unwrap()
|
||||||
|
.get_port::<dyn SingletonView<Item = char>>().unwrap()
|
||||||
|
.map(
|
||||||
|
|c| TypeTerm::Char(c)
|
||||||
|
)
|
||||||
|
.into()
|
||||||
|
);
|
||||||
|
|
||||||
node
|
node
|
||||||
}
|
}
|
||||||
State::List => {
|
State::List => {
|
||||||
|
@ -106,6 +121,18 @@ impl TypeTermEditor {
|
||||||
PTYListController::for_node( &mut node, Some(' '), Some('>') );
|
PTYListController::for_node( &mut node, Some(' '), Some('>') );
|
||||||
PTYListStyle::for_node( &mut node, ("<"," ",">") );
|
PTYListStyle::for_node( &mut node, ("<"," ",">") );
|
||||||
|
|
||||||
|
self.data.write().unwrap().insert_leaf(
|
||||||
|
vec![].into_iter(),
|
||||||
|
node.data.clone().unwrap().read().unwrap()
|
||||||
|
.get_port::<dyn SequenceView<Item = NestedNode>>().unwrap()
|
||||||
|
.map(
|
||||||
|
|node| {
|
||||||
|
node.data.as_ref().unwrap().read().unwrap().get_port::<dyn SingletonView<Item = TypeTerm>>().unwrap()
|
||||||
|
}
|
||||||
|
)
|
||||||
|
.into()
|
||||||
|
);
|
||||||
|
|
||||||
node
|
node
|
||||||
}
|
}
|
||||||
State::Symbol => {
|
State::Symbol => {
|
||||||
|
@ -131,9 +158,16 @@ impl TypeTermEditor {
|
||||||
}
|
}
|
||||||
|
|
||||||
fn with_node(ctx: Arc<RwLock<Context>>, depth: usize, node: NestedNode, state: State) -> NestedNode {
|
fn with_node(ctx: Arc<RwLock<Context>>, depth: usize, node: NestedNode, state: State) -> NestedNode {
|
||||||
|
let buffer = SingletonBuffer::<Option<TypeTerm>>::new( None );
|
||||||
|
|
||||||
|
let data = Arc::new(RwLock::new(ReprTree::new(
|
||||||
|
(&ctx, "( TypeTerm )")
|
||||||
|
)));
|
||||||
|
|
||||||
let mut editor = TypeTermEditor {
|
let mut editor = TypeTermEditor {
|
||||||
ctx: ctx.clone(),
|
ctx: ctx.clone(),
|
||||||
state,
|
state,
|
||||||
|
data: data.clone(),
|
||||||
cur_node: SingletonBuffer::new(node),
|
cur_node: SingletonBuffer::new(node),
|
||||||
editor: SingletonBuffer::new(None)
|
editor: SingletonBuffer::new(None)
|
||||||
};
|
};
|
||||||
|
@ -161,14 +195,54 @@ impl TypeTermEditor {
|
||||||
let mut node = NestedNode::new(depth)
|
let mut node = NestedNode::new(depth)
|
||||||
.set_ctx(ctx)
|
.set_ctx(ctx)
|
||||||
.set_view(view)
|
.set_view(view)
|
||||||
|
.set_data(data)
|
||||||
.set_nav(editor.clone())
|
.set_nav(editor.clone())
|
||||||
.set_cmd(editor.clone())
|
.set_cmd(editor.clone())
|
||||||
.set_editor(editor.clone());
|
.set_editor(editor.clone());
|
||||||
|
|
||||||
|
node.close_char.set(cc.get());
|
||||||
editor.write().unwrap().editor = node.editor.clone();
|
editor.write().unwrap().editor = node.editor.clone();
|
||||||
|
|
||||||
node
|
node
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn get_typeterm(&self) -> Option<TypeTerm> {
|
||||||
|
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 {
|
impl TreeNav for TypeTermEditor {
|
||||||
|
@ -252,6 +326,8 @@ impl ObjCommander for TypeTermEditor {
|
||||||
}
|
}
|
||||||
|
|
||||||
State::List => {
|
State::List => {
|
||||||
|
self.cur_node.get_mut().send_cmd_obj( co )
|
||||||
|
/*
|
||||||
match self.cur_node.get_mut().send_cmd_obj( co ) {
|
match self.cur_node.get_mut().send_cmd_obj( co ) {
|
||||||
TreeNavResult::Continue => {
|
TreeNavResult::Continue => {
|
||||||
TreeNavResult::Continue
|
TreeNavResult::Continue
|
||||||
|
@ -277,9 +353,10 @@ impl ObjCommander for TypeTermEditor {
|
||||||
_ => {
|
_ => {
|
||||||
TreeNavResult::Exit
|
TreeNavResult::Exit
|
||||||
}
|
}
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
}
|
||||||
|
*/
|
||||||
}
|
}
|
||||||
|
|
||||||
_ => {
|
_ => {
|
||||||
|
@ -290,7 +367,17 @@ impl ObjCommander for TypeTermEditor {
|
||||||
TreeNavResult::Exit
|
TreeNavResult::Exit
|
||||||
}
|
}
|
||||||
} else {
|
} 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 )
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -61,7 +61,7 @@ impl TypeLadder {
|
||||||
s = s + "~";
|
s = s + "~";
|
||||||
}
|
}
|
||||||
first = false;
|
first = false;
|
||||||
s = s + &t.to_str1(names);
|
s = s + &t.to_str(names);
|
||||||
}
|
}
|
||||||
s
|
s
|
||||||
}
|
}
|
||||||
|
|
|
@ -22,10 +22,8 @@ pub fn init_mem_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
"Vec", Arc::new(
|
"Vec", Arc::new(
|
||||||
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| {
|
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| {
|
||||||
match ty {
|
match ty {
|
||||||
TypeTerm::Type {
|
TypeTerm::App(args) => {
|
||||||
id: _, args
|
if args.len() > 1 {
|
||||||
} => {
|
|
||||||
if args.len() > 0 {
|
|
||||||
let buf = r3vi::buffer::vec::VecBuffer::<char>::new();
|
let buf = r3vi::buffer::vec::VecBuffer::<char>::new();
|
||||||
let data = ReprTree::new_leaf(
|
let data = ReprTree::new_leaf(
|
||||||
ctx.read().unwrap().type_term_from_str("( Char )").unwrap(),
|
ctx.read().unwrap().type_term_from_str("( Char )").unwrap(),
|
||||||
|
@ -52,9 +50,12 @@ 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 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(
|
"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))
|
||||||
|
@ -62,50 +63,51 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
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 {
|
let pattern = MorphismTypePattern {
|
||||||
src_tyid: ctx.read().unwrap().get_typeid("List"),
|
src_tyid: ctx.get_typeid("List"),
|
||||||
dst_tyid: ctx.read().unwrap().get_typeid("Symbol").unwrap()
|
dst_tyid: ctx.get_typeid("Symbol").unwrap()
|
||||||
};
|
};
|
||||||
ctx.write().unwrap().add_morphism(pattern,
|
ctx.add_morphism(pattern,
|
||||||
Arc::new(
|
Arc::new(
|
||||||
|mut node, _dst_type:_| {
|
|mut node, _dst_type:_| {
|
||||||
PTYListController::for_node( &mut node, None, None );
|
PTYListController::for_node( &mut node, None, None );
|
||||||
PTYListStyle::for_node( &mut node, ("","","") );
|
PTYListStyle::for_node( &mut node, ("","","") );
|
||||||
|
|
||||||
Some(node)
|
Some(node)
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write().unwrap().add_node_ctor(
|
ctx.add_node_ctor(
|
||||||
"Symbol", Arc::new(
|
"Symbol", Arc::new(
|
||||||
|ctx: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
|
|ctx: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
|
||||||
let mut node = Context::make_node(
|
let mut node = Context::make_node(
|
||||||
&ctx,
|
&ctx,
|
||||||
(&ctx, "( List Char )").into(),
|
(&ctx, "( List Char )").into(),
|
||||||
depth+1
|
depth+1
|
||||||
).unwrap();
|
).expect("nested node");
|
||||||
|
|
||||||
node = node.morph(dst_typ);
|
//node = node.morph(dst_typ);
|
||||||
|
|
||||||
Some(node)
|
Some(node)
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write().unwrap().add_list_typename("String".into());
|
ctx.add_list_typename("String".into());
|
||||||
let pattern = MorphismTypePattern {
|
let pattern = MorphismTypePattern {
|
||||||
src_tyid: ctx.read().unwrap().get_typeid("List"),
|
src_tyid: ctx.get_typeid("List"),
|
||||||
dst_tyid: ctx.read().unwrap().get_typeid("String").unwrap()
|
dst_tyid: ctx.get_typeid("String").unwrap()
|
||||||
};
|
};
|
||||||
ctx.write().unwrap().add_morphism(pattern,
|
ctx.add_morphism(pattern,
|
||||||
Arc::new(
|
Arc::new(
|
||||||
|mut node, _dst_type:_| {
|
|mut node, _dst_type:_| {
|
||||||
PTYListController::for_node( &mut node, None, Some('\"') );
|
PTYListController::for_node( &mut node, None, Some('\"') );
|
||||||
|
@ -115,17 +117,15 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write().unwrap().add_node_ctor(
|
ctx.add_node_ctor(
|
||||||
"String", Arc::new(
|
"String", Arc::new(
|
||||||
|ctx: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
|
|ctx: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
|
||||||
let mut node = Context::make_node(
|
let mut node = Context::make_node(
|
||||||
&ctx,
|
&ctx,
|
||||||
TypeTerm::Type {
|
TypeTerm::App(vec![
|
||||||
id: ctx.read().unwrap().get_fun_typeid("List").unwrap(),
|
TypeTerm::TypeID(ctx.read().unwrap().get_typeid("List").unwrap()),
|
||||||
args: vec![
|
TypeTerm::new(ctx.read().unwrap().get_typeid("Char").unwrap())
|
||||||
TypeTerm::new(ctx.read().unwrap().get_typeid("Char").unwrap()).into()
|
]),
|
||||||
]
|
|
||||||
},
|
|
||||||
depth+1
|
depth+1
|
||||||
).unwrap();
|
).unwrap();
|
||||||
|
|
||||||
|
@ -136,8 +136,8 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
/*
|
/*
|
||||||
ctx.write().unwrap().add_list_typename("TypeTerm".into());
|
ctx.add_list_typename("TypeTerm".into());
|
||||||
ctx.write().unwrap().add_node_ctor(
|
ctx.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(depth))
|
Some(TypeTermEditor::new(ctx, depth).into_node(depth))
|
||||||
|
@ -145,27 +145,29 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
*/
|
*/
|
||||||
ctx.write().unwrap().add_typename("TerminalEvent".into());
|
ctx.add_typename("TerminalEvent".into());
|
||||||
ctx
|
|
||||||
|
drop(ctx);
|
||||||
|
ctx0
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
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());
|
let mut ctx = ctx0.write().unwrap();
|
||||||
ctx.write().unwrap().add_typename("u32".into());
|
ctx.add_typename("MachineInt".into());
|
||||||
ctx.write().unwrap().add_typename("LittleEndian".into());
|
ctx.add_typename("u32".into());
|
||||||
ctx.write().unwrap().add_typename("BigEndian".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(
|
"Digit", Arc::new(
|
||||||
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| {
|
|ctx: Arc<RwLock<Context>>, ty: TypeTerm, depth: usize| {
|
||||||
match ty {
|
match ty {
|
||||||
TypeTerm::Type {
|
TypeTerm::App(args) => {
|
||||||
id: _, args
|
if args.len() > 1 {
|
||||||
} => {
|
match args[1] {
|
||||||
if args.len() > 0 {
|
|
||||||
match (args[0].0)[0] {
|
|
||||||
TypeTerm::Num(radix) => {
|
TypeTerm::Num(radix) => {
|
||||||
let node = DigitEditor::new(ctx.clone(), radix as u32).into_node(depth);
|
let node = DigitEditor::new(ctx.clone(), radix as u32).into_node(depth);
|
||||||
Some(
|
Some(
|
||||||
|
@ -184,25 +186,23 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write().unwrap().add_list_typename("PosInt".into());
|
ctx.add_list_typename("PosInt".into());
|
||||||
let pattern = MorphismTypePattern {
|
let pattern = MorphismTypePattern {
|
||||||
src_tyid: ctx.read().unwrap().get_typeid("List"),
|
src_tyid: ctx.get_typeid("List"),
|
||||||
dst_tyid: ctx.read().unwrap().get_typeid("PosInt").unwrap()
|
dst_tyid: ctx.get_typeid("PosInt").unwrap()
|
||||||
};
|
};
|
||||||
ctx.write().unwrap().add_morphism(pattern,
|
ctx.add_morphism(pattern,
|
||||||
Arc::new(
|
Arc::new(
|
||||||
|mut node, dst_type| {
|
|mut node, dst_type| {
|
||||||
let depth = node.depth.get();
|
let depth = node.depth.get();
|
||||||
let editor = node.editor.get().unwrap().downcast::<RwLock<ListEditor>>().unwrap();
|
let editor = node.editor.get().unwrap().downcast::<RwLock<ListEditor>>().unwrap();
|
||||||
|
|
||||||
// todo: check src_type parameter to be ( Digit radix )
|
// todo: check src_type parameter to be ( Digit radix )
|
||||||
|
|
||||||
match dst_type {
|
match dst_type {
|
||||||
TypeTerm::Type {
|
TypeTerm::App(args) => {
|
||||||
id: _, args
|
if args.len() > 1 {
|
||||||
} => {
|
match args[1] {
|
||||||
if args.len() > 0 {
|
|
||||||
match (args[0].0)[0] {
|
|
||||||
TypeTerm::Num(_radix) => {
|
TypeTerm::Num(_radix) => {
|
||||||
PTYListController::for_node(
|
PTYListController::for_node(
|
||||||
&mut node,
|
&mut node,
|
||||||
|
@ -229,28 +229,26 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write().unwrap().add_node_ctor(
|
ctx.add_node_ctor(
|
||||||
"PosInt", Arc::new(
|
"PosInt", Arc::new(
|
||||||
|ctx: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
|
|ctx0: Arc<RwLock<Context>>, dst_typ: TypeTerm, depth: usize| {
|
||||||
match dst_typ.clone() {
|
match dst_typ.clone() {
|
||||||
TypeTerm::Type {
|
TypeTerm::App(args) => {
|
||||||
id: _, args
|
if args.len() > 1 {
|
||||||
} => {
|
match args[1] {
|
||||||
if args.len() > 0 {
|
|
||||||
match (args[0].0)[0] {
|
|
||||||
TypeTerm::Num(radix) => {
|
TypeTerm::Num(radix) => {
|
||||||
|
let ctx = ctx0.read().unwrap();
|
||||||
let mut node = Context::make_node(
|
let mut node = Context::make_node(
|
||||||
&ctx,
|
&ctx0,
|
||||||
TypeTerm::Type {
|
TypeTerm::App(vec![
|
||||||
id: ctx.read().unwrap().get_fun_typeid("List").unwrap(),
|
TypeTerm::TypeID(ctx.get_typeid("List").unwrap()),
|
||||||
args: vec![
|
TypeTerm::TypeID(
|
||||||
TypeTerm::new(ctx.read().unwrap().get_typeid("Digit").unwrap())
|
ctx.get_typeid("Digit").unwrap()
|
||||||
.num_arg(radix)
|
)
|
||||||
.clone()
|
.num_arg(radix)
|
||||||
.into()
|
.clone()
|
||||||
]
|
.into()
|
||||||
},
|
]),
|
||||||
depth+1
|
depth+1
|
||||||
).unwrap();
|
).unwrap();
|
||||||
|
|
||||||
|
@ -269,52 +267,15 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
);
|
);
|
||||||
|
|
||||||
ctx.write().unwrap().add_list_typename("RGB".into());
|
|
||||||
ctx.write().unwrap().add_node_ctor(
|
|
||||||
"RGB", Arc::new(
|
|
||||||
|ctx: Arc<RwLock<Context>>, _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
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -2,14 +2,14 @@ pub mod context;
|
||||||
|
|
||||||
pub mod dict;
|
pub mod dict;
|
||||||
pub mod term;
|
pub mod term;
|
||||||
pub mod ladder;
|
//pub mod ladder;
|
||||||
pub mod repr_tree;
|
pub mod repr_tree;
|
||||||
pub mod make_editor;
|
pub mod make_editor;
|
||||||
pub mod editor;
|
pub mod editor;
|
||||||
|
|
||||||
pub use {
|
pub use {
|
||||||
dict::*,
|
dict::*,
|
||||||
ladder::*,
|
// ladder::*,
|
||||||
repr_tree::*,
|
repr_tree::*,
|
||||||
term::*,
|
term::*,
|
||||||
context::{Context, MorphismMode, MorphismType, MorphismTypePattern},
|
context::{Context, MorphismMode, MorphismType, MorphismTypePattern},
|
||||||
|
|
|
@ -89,8 +89,7 @@ impl ReprTree {
|
||||||
self.port
|
self.port
|
||||||
.clone()?
|
.clone()?
|
||||||
.downcast::<V>()
|
.downcast::<V>()
|
||||||
.ok()
|
.ok()?
|
||||||
.unwrap()
|
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -1,43 +1,54 @@
|
||||||
use {
|
use {
|
||||||
crate::{
|
crate::{
|
||||||
type_system::{TypeLadder, TypeID}
|
type_system::{TypeID}
|
||||||
},
|
},
|
||||||
std::collections::HashMap
|
std::collections::HashMap
|
||||||
};
|
};
|
||||||
|
|
||||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||||
|
|
||||||
|
|
||||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||||
pub enum TypeTerm {
|
pub enum TypeTerm {
|
||||||
/* TODO: refactor into this:
|
/* Atomic Terms */
|
||||||
Nominal {
|
|
||||||
id: u64,
|
// Base types from dictionary
|
||||||
args: Vec< TypeTerm >
|
TypeID(TypeID),
|
||||||
},
|
|
||||||
Ladder(Vec< TypeTerm >),
|
// Literals
|
||||||
*/
|
|
||||||
Type {
|
|
||||||
id: u64,
|
|
||||||
args: Vec< TypeLadder >
|
|
||||||
},
|
|
||||||
Var(u64),
|
|
||||||
Num(i64),
|
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 {
|
impl TypeTerm {
|
||||||
pub fn new(id: TypeID) -> Self {
|
pub fn new(id: TypeID) -> Self {
|
||||||
match id {
|
TypeTerm::TypeID(id)
|
||||||
TypeID::Fun(id) => TypeTerm::Type { id, args: vec![] },
|
|
||||||
TypeID::Var(_) => {unreachable!();}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn arg(&mut self, t: impl Into<TypeLadder>) -> &mut Self {
|
pub fn arg(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
|
||||||
if let TypeTerm::Type { id: _, args } = self {
|
match self {
|
||||||
args.push(t.into());
|
TypeTerm::App(args) => {
|
||||||
|
args.push(t.into());
|
||||||
|
}
|
||||||
|
|
||||||
|
_ => {
|
||||||
|
*self = TypeTerm::App(vec![
|
||||||
|
self.clone(),
|
||||||
|
t.into()
|
||||||
|
])
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
self
|
self
|
||||||
|
@ -51,6 +62,29 @@ impl TypeTerm {
|
||||||
self.arg(TypeTerm::Char(c))
|
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<String, TypeID>) -> Option<Self> {
|
pub fn from_str(s: &str, names: &HashMap<String, TypeID>) -> Option<Self> {
|
||||||
let mut term_stack = Vec::<Option<TypeTerm>>::new();
|
let mut term_stack = Vec::<Option<TypeTerm>>::new();
|
||||||
|
|
||||||
|
@ -111,53 +145,42 @@ impl TypeTerm {
|
||||||
None
|
None
|
||||||
}
|
}
|
||||||
|
|
||||||
// only adds parenthesis where args.len > 0
|
pub fn to_str(&self, names: &HashMap<TypeID, String>) -> String {
|
||||||
pub fn to_str1(&self, names: &HashMap<TypeID, String>) -> String {
|
|
||||||
match self {
|
match self {
|
||||||
TypeTerm::Type { id, args } => {
|
TypeTerm::App(args) => {
|
||||||
if args.len() > 0 {
|
let mut out = String::new();
|
||||||
format!(
|
|
||||||
"<{}{}>",
|
out.push_str(&"<");
|
||||||
names[&TypeID::Fun(*id)],
|
|
||||||
if args.len() > 0 {
|
for x in args.iter() {
|
||||||
args.iter().fold(String::new(), |str, term| {
|
out.push_str(&" ");
|
||||||
format!("{} {}", str, term.to_str1(names))
|
out.push_str(&x.to_str(names));
|
||||||
})
|
|
||||||
} else {
|
|
||||||
String::new()
|
|
||||||
}
|
|
||||||
)
|
|
||||||
} else {
|
|
||||||
names[&TypeID::Fun(*id)].clone()
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
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::Num(n) => format!("{}", n),
|
||||||
TypeTerm::Char('\n') => format!("'\\n'"),
|
TypeTerm::Char('\n') => format!("'\\n'"),
|
||||||
TypeTerm::Char(c) => format!("'{}'", c),
|
TypeTerm::Char(c) => format!("'{}'", c),
|
||||||
TypeTerm::Var(varid) => format!("T"),
|
TypeTerm::TypeID(id) => format!("{}", names[id]),
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// always adds an enclosing pair of parenthesis
|
|
||||||
pub fn to_str(&self, names: &HashMap<TypeID, String>) -> 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"),
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue