implement first typelader-compatibility algorithm
This commit is contained in:
parent
57682826f8
commit
4b6cc1ee55
6 changed files with 61 additions and 13 deletions
|
@ -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])))));
|
||||
b.push(crate::diagnostics::make_todo(crate::terminal::make_label(&format!("complete {}", self.ctx.read().unwrap().type_term_to_str(&n.0[0])))));
|
||||
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])))));
|
||||
b.push(crate::diagnostics::make_todo(crate::terminal::make_label(&format!("complete {}", self.ctx.read().unwrap().type_term_to_str(&t.0[0])))));
|
||||
|
||||
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].clone(), *ed_depth+1).unwrap();
|
||||
let mut e = Context::make_node(&self.ctx, t.0[0].clone(), *ed_depth+1).unwrap();
|
||||
*editor = Some(e.clone());
|
||||
update_segment = true;
|
||||
|
||||
|
|
|
@ -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].clone(), *ed_depth+1).unwrap();
|
||||
let mut e = Context::make_node(&self.ctx, t.0[0].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].clone(), *ed_depth+1).unwrap();
|
||||
let mut e = Context::make_node(&self.ctx, t.0[0].clone(), *ed_depth+1).unwrap();
|
||||
*editor = Some(e.clone());
|
||||
e.goby(direction);
|
||||
}
|
||||
|
|
|
@ -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]))
|
||||
make_label(&ctx.read().unwrap().type_term_to_str(&t.0[0]))
|
||||
.map_item({
|
||||
let _cur_depth = *cur_depth;
|
||||
let _ed_depth = *ed_depth;
|
||||
|
|
|
@ -8,7 +8,7 @@ use {
|
|||
|
||||
pub trait TreeType {
|
||||
fn get_type(&self, _addr: &TreeAddr) -> TypeLadder {
|
||||
vec![]
|
||||
vec![].into()
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -61,6 +61,7 @@ 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("List".into());
|
||||
|
@ -203,6 +204,7 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
|
||||
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());
|
||||
|
||||
ctx.write().unwrap().add_node_ctor(
|
||||
|
@ -330,17 +332,17 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
.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();
|
||||
|
@ -359,6 +361,13 @@ pub fn init_math_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
}
|
||||
));
|
||||
|
||||
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
|
||||
}
|
||||
|
||||
|
|
|
@ -3,7 +3,46 @@ use {crate::utils::Bimap, std::collections::HashMap};
|
|||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
pub type TypeID = u64;
|
||||
pub type TypeLadder = Vec<TypeTerm>;
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct TypeLadder(pub Vec<TypeTerm>);
|
||||
|
||||
impl From<Vec<TypeTerm>> for TypeLadder {
|
||||
fn from(l: Vec<TypeTerm>) -> Self {
|
||||
TypeLadder(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)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
|
@ -107,7 +146,7 @@ impl TypeTerm {
|
|||
pub fn to_str(&self, names: &HashMap<u64, String>) -> String {
|
||||
match self {
|
||||
TypeTerm::Type { id, args } => format!(
|
||||
"« {} {}»",
|
||||
"( {} {})",
|
||||
names[id],
|
||||
if args.len() > 0 {
|
||||
args.iter().fold(String::new(), |str, term| {
|
||||
|
|
Loading…
Reference in a new issue