From 17b58e6bcad02d1e71fc817149fdccc8a31d28c4 Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Thu, 2 Mar 2023 03:43:38 +0100 Subject: [PATCH] TypeTerm: type-ladder arguments, variables & char-literals --- nested/src/editors/integer/editor.rs | 8 +- nested/src/editors/list/editor.rs | 4 +- nested/src/type_system/context.rs | 26 +++- nested/src/type_system/dict.rs | 71 +++++++++ .../{type_term_editor.rs => editor.rs} | 0 nested/src/type_system/ladder.rs | 71 +++++++++ nested/src/type_system/make_editor.rs | 15 +- nested/src/type_system/mod.rs | 16 +- .../src/type_system/{type_term.rs => term.rs} | 141 +++++------------- 9 files changed, 224 insertions(+), 128 deletions(-) create mode 100644 nested/src/type_system/dict.rs rename nested/src/type_system/{type_term_editor.rs => editor.rs} (100%) create mode 100644 nested/src/type_system/ladder.rs rename nested/src/type_system/{type_term.rs => term.rs} (50%) diff --git a/nested/src/editors/integer/editor.rs b/nested/src/editors/integer/editor.rs index d324017..89e9a9c 100644 --- a/nested/src/editors/integer/editor.rs +++ b/nested/src/editors/integer/editor.rs @@ -116,7 +116,7 @@ impl DigitEditor { TypeTerm::Type { id: self.ctx.read().unwrap().get_typeid("Digit").unwrap(), args: vec![ - TypeTerm::Num(self.radix as i64) + TypeTerm::Num(self.radix as i64).into() ] } } @@ -145,7 +145,7 @@ impl PosIntEditor { TypeTerm::Type { id: ctx.read().unwrap().get_typeid("Digit").unwrap(), args: vec![ - TypeTerm::Num(radix as i64) + TypeTerm::Num(radix as i64).into() ] }, None, @@ -169,11 +169,11 @@ impl PosIntEditor { TypeTerm::Type { id: ctx.read().unwrap().get_typeid("PosInt").unwrap(), args: vec![ - TypeTerm::Num(radix as i64), + TypeTerm::Num(radix as i64).into(), TypeTerm::Type { id: ctx.read().unwrap().get_typeid("BigEndian").unwrap(), args: vec![] - } + }.into() ] } )); diff --git a/nested/src/editors/list/editor.rs b/nested/src/editors/list/editor.rs index c96e1e2..0c28269 100644 --- a/nested/src/editors/list/editor.rs +++ b/nested/src/editors/list/editor.rs @@ -125,8 +125,8 @@ impl ListEditor { pub fn get_seq_type(&self) -> TypeTerm { TypeTerm::Type { id: self.ctx.read().unwrap().get_typeid("List").unwrap(), - args: vec![ self.get_item_type() ] - } + args: vec![ self.get_item_type().into() ] + } } pub fn get_cursor_port(&self) -> OuterViewPort> { diff --git a/nested/src/type_system/context.rs b/nested/src/type_system/context.rs index 5d5bec1..cf9fd85 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}, + type_system::{TypeDict, TypeTerm, TypeID, ReprTree, TypeLadder}, tree::NestedNode }, std::{ @@ -11,8 +11,6 @@ use { //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> -pub struct TypeLadder(Vec); - #[derive(Clone, Copy, Hash, PartialEq, Eq)] pub enum MorphismMode { /// Isomorphism @@ -50,12 +48,12 @@ impl From for MorphismTypePattern { fn from(value: MorphismType) -> MorphismTypePattern { MorphismTypePattern { src_tyid: match value.src_type { - Some(TypeTerm::Type { id, args: _ }) => Some(id), + Some(TypeTerm::Type { id, args: _ }) => Some(TypeID::Fun(id)), _ => None, }, dst_tyid: match value.dst_type { - TypeTerm::Type { id, args: _ } => id, + TypeTerm::Type { id, args: _ } => TypeID::Fun(id), _ => unreachable!() } } @@ -66,7 +64,7 @@ impl From for MorphismTypePattern { pub struct Context { /// assigns a name to every type - type_dict: Arc>, + pub type_dict: Arc>, /// named vertices of the graph nodes: HashMap< String, NestedNode >, @@ -135,7 +133,7 @@ impl Context { pub fn is_list_type(&self, t: &TypeTerm) -> bool { match t { TypeTerm::Type { id, args: _ } => { - self.list_types.contains(id) + self.list_types.contains(&TypeID::Fun(*id)) } _ => false } @@ -145,6 +143,20 @@ impl Context { self.type_dict.read().unwrap().get_typeid(&tn.into()) } + pub fn get_fun_typeid(&self, tn: &str) -> Option { + match self.get_typeid(tn) { + Some(TypeID::Fun(x)) => Some(x), + _ => None + } + } + + pub fn get_var_typeid(&self, tn: &str) -> Option { + match self.get_typeid(tn) { + Some(TypeID::Var(x)) => Some(x), + _ => None + } + } + pub fn type_term_from_str(&self, tn: &str) -> Option { self.type_dict.read().unwrap().type_term_from_str(&tn) } diff --git a/nested/src/type_system/dict.rs b/nested/src/type_system/dict.rs new file mode 100644 index 0000000..7ef52f6 --- /dev/null +++ b/nested/src/type_system/dict.rs @@ -0,0 +1,71 @@ +use { + crate::{ + utils::Bimap, + type_system::{TypeTerm, TypeLadder} + } +}; + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + +#[derive(Eq, PartialEq, Hash, Clone, Debug)] +pub enum TypeID { + Fun(u64), + Var(u64) +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + +pub struct TypeDict { + typenames: Bimap, + type_lit_counter: u64, + type_var_counter: u64, +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + +impl TypeDict { + pub fn new() -> Self { + TypeDict { + typenames: Bimap::new(), + type_lit_counter: 0, + type_var_counter: 0, + } + } + + pub fn add_varname(&mut self, tn: String) -> TypeID { + let tyid = TypeID::Var(self.type_var_counter); + self.type_var_counter += 1; + self.typenames.insert(tn, tyid.clone()); + tyid + } + + pub fn add_typename(&mut self, tn: String) -> TypeID { + let tyid = TypeID::Fun(self.type_lit_counter); + self.type_lit_counter += 1; + self.typenames.insert(tn, tyid.clone()); + tyid + } + + pub fn get_typename(&self, tid: &TypeID) -> Option { + self.typenames.my.get(tid).cloned() + } + + pub fn get_typeid(&self, tn: &String) -> Option { + self.typenames.mλ.get(tn).cloned() + } + + pub fn type_term_from_str(&self, typename: &str) -> Option { + TypeTerm::from_str(typename, &self.typenames.mλ) + } + + 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/type_term_editor.rs b/nested/src/type_system/editor.rs similarity index 100% rename from nested/src/type_system/type_term_editor.rs rename to nested/src/type_system/editor.rs diff --git a/nested/src/type_system/ladder.rs b/nested/src/type_system/ladder.rs new file mode 100644 index 0000000..d730452 --- /dev/null +++ b/nested/src/type_system/ladder.rs @@ -0,0 +1,71 @@ +use { + crate::type_system::{TypeTerm, TypeID}, + std::collections::HashMap +}; + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + +#[derive(Clone, Eq, PartialEq, Hash, Debug)] +pub struct TypeLadder(pub Vec); + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + +impl From> for TypeLadder { + fn from(l: Vec) -> Self { + TypeLadder(l) + } +} + +impl From for TypeLadder { + fn from(l: TypeTerm) -> Self { + TypeLadder(vec![ l ]) + } +} + +impl TypeLadder { + /// if compatible, returns the number of descents neccesary + pub fn is_compatible_with(&self, other: &TypeLadder) -> Option { + 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> { + if let Some(start) = self.is_compatible_with(other) { + for (i, (t1, t2)) in self.0.iter().skip(start).zip(other.0.iter()).enumerate() { + if t1 != t2 { + return Err(Some((start, i))); + } + } + + Ok(start) + } else { + Err(None) + } + } + + pub fn to_str1(&self, names: &HashMap) -> String { + let mut s = String::new(); + let mut first = true; + + for t in self.0.iter() { + if !first { + s = s + "~"; + } + first = false; + s = s + &t.to_str1(names); + } + s + } +} + +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + diff --git a/nested/src/type_system/make_editor.rs b/nested/src/type_system/make_editor.rs index 9e5b02c..5da6a09 100644 --- a/nested/src/type_system/make_editor.rs +++ b/nested/src/type_system/make_editor.rs @@ -75,7 +75,7 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { if args.len() > 0 { let editor = PTYListEditor::new( ctx, - args[0].clone(), + (args[0].clone().0)[0].clone(), Some(','), depth + 1 ); @@ -125,7 +125,7 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { TypeTerm::Type { id: 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 @@ -173,7 +173,7 @@ pub fn init_editor_ctx(parent: Arc>) -> Arc> { TypeTerm::Type { id: 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 @@ -215,9 +215,9 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { id: _, args } => { if args.len() > 0 { - match args[0] { + match (args[0].0)[0] { 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( node ) @@ -252,7 +252,7 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { id: _, args } => { if args.len() > 0 { - match args[0] { + match (args[0].0)[0] { TypeTerm::Num(_radix) => { let pty_editor = PTYListEditor::from_editor( editor, @@ -291,7 +291,7 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { id: _, args } => { if args.len() > 0 { - match args[0] { + match (args[0].0)[0] { TypeTerm::Num(radix) => { let mut node = Context::make_node( @@ -302,6 +302,7 @@ pub fn init_math_ctx(parent: Arc>) -> Arc> { TypeTerm::new(ctx.read().unwrap().get_typeid("Digit").unwrap()) .num_arg(radix) .clone() + .into() ] }, depth+1 diff --git a/nested/src/type_system/mod.rs b/nested/src/type_system/mod.rs index a4c590a..4446a91 100644 --- a/nested/src/type_system/mod.rs +++ b/nested/src/type_system/mod.rs @@ -1,13 +1,17 @@ - -pub mod type_term; -pub mod repr_tree; pub mod context; + +pub mod dict; +pub mod term; +pub mod ladder; +pub mod repr_tree; pub mod make_editor; -//pub mod type_term_editor; +//pub mod editor; pub use { - repr_tree::{ReprTree}, - type_term::{TypeDict, TypeID, TypeTerm, TypeLadder}, + dict::*, + ladder::*, + repr_tree::*, + term::*, context::{Context, MorphismMode, MorphismType, MorphismTypePattern}, // type_term_editor::TypeTermEditor, make_editor::* diff --git a/nested/src/type_system/type_term.rs b/nested/src/type_system/term.rs similarity index 50% rename from nested/src/type_system/type_term.rs rename to nested/src/type_system/term.rs index bae86b6..056b0be 100644 --- a/nested/src/type_system/type_term.rs +++ b/nested/src/type_system/term.rs @@ -1,66 +1,36 @@ -use {crate::utils::Bimap, std::collections::HashMap}; - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -pub type TypeID = u64; - -#[derive(Clone)] -pub struct TypeLadder(pub Vec); - -impl From> for TypeLadder { - fn from(l: Vec) -> Self { - TypeLadder(l) - } -} - -impl TypeLadder { - /// if compatible, returns the number of descents neccesary - pub fn is_compatible_with(&self, other: &TypeLadder) -> Option { - 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> { - 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) - } - } -} +use { + crate::{ + type_system::{TypeLadder, TypeID} + }, + std::collections::HashMap +}; //<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> #[derive(Clone, PartialEq, Eq, Hash, Debug)] pub enum TypeTerm { - Type { id: TypeID, args: Vec }, + Type { + id: u64, + args: Vec< TypeLadder > + }, + Var(u64), Num(i64), -// Var(u64), + Char(char) } +//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> + impl TypeTerm { pub fn new(id: TypeID) -> Self { - TypeTerm::Type { id, args: vec![] } + match id { + TypeID::Fun(id) => TypeTerm::Type { id, args: vec![] }, + TypeID::Var(_) => {unreachable!();} + } } - pub fn arg(&mut self, t: TypeTerm) -> &mut Self { + pub fn arg(&mut self, t: impl Into) -> &mut Self { if let TypeTerm::Type { id: _, args } = self { - args.push(t); + args.push(t.into()); } self @@ -69,8 +39,12 @@ impl TypeTerm { pub fn num_arg(&mut self, v: i64) -> &mut Self { self.arg(TypeTerm::Num(v)) } - - pub fn from_str(s: &str, names: &HashMap) -> Option { + + pub fn char_arg(&mut self, c: char) -> &mut Self { + self.arg(TypeTerm::Char(c)) + } + + pub fn from_str(s: &str, names: &HashMap) -> Option { let mut term_stack = Vec::>::new(); for token in s.split_whitespace() { @@ -100,13 +74,13 @@ impl TypeTerm { f.num_arg(i64::from_str_radix(atom, 10).unwrap()); } else { f.arg(TypeTerm::new( - *names.get(atom).expect(&format!("invalid atom {}", atom)), + names.get(atom).expect(&format!("invalid atom {}", atom)).clone(), )); } } None => { *f = Some(TypeTerm::new( - *names.get(atom).expect(&format!("invalid atom {}", atom)), + names.get(atom).expect(&format!("invalid atom {}", atom)).clone(), )); } } @@ -118,36 +92,38 @@ impl TypeTerm { } // only adds parenthesis where args.len > 0 - pub fn to_str1(&self, names: &HashMap) -> String { + pub fn to_str1(&self, names: &HashMap) -> String { match self { TypeTerm::Type { id, args } => { if args.len() > 0 { format!( - "( {} {})", - names[id], + "({}{})", + names[&TypeID::Fun(*id)], if args.len() > 0 { args.iter().fold(String::new(), |str, term| { - format!("{}{} ", str, term.to_str1(names)) + format!(" {}{}", str, term.to_str1(names)) }) } else { String::new() } ) } else { - names[id].clone() + names[&TypeID::Fun(*id)].clone() } } TypeTerm::Num(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 { + pub fn to_str(&self, names: &HashMap) -> String { match self { TypeTerm::Type { id, args } => format!( "( {} {})", - names[id], + names[&TypeID::Fun(*id)], if args.len() > 0 { args.iter().fold(String::new(), |str, term| { format!("{}{} ", str, term.to_str1(names)) @@ -158,47 +134,8 @@ impl TypeTerm { ), TypeTerm::Num(n) => format!("{}", n), + TypeTerm::Char(c) => format!("'{}'", c), + TypeTerm::Var(varid) => format!("T"), } } } - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>> - -pub struct TypeDict { - typenames: Bimap, - type_id_counter: TypeID, -} - -impl TypeDict { - pub fn new() -> Self { - TypeDict { - typenames: Bimap::new(), - type_id_counter: 0, - } - } - - pub fn add_typename(&mut self, tn: String) -> TypeID { - let tyid = self.type_id_counter; - self.type_id_counter += 1; - self.typenames.insert(tn, tyid); - tyid - } - - pub fn get_typename(&self, tid: &u64) -> Option { - self.typenames.my.get(tid).cloned() - } - - pub fn get_typeid(&self, tn: &String) -> Option { - self.typenames.mλ.get(tn).cloned() - } - - pub fn type_term_from_str(&self, typename: &str) -> Option { - TypeTerm::from_str(typename, &self.typenames.mλ) - } - - pub fn type_term_to_str(&self, term: &TypeTerm) -> String { - term.to_str(&self.typenames.my) - } -} - -//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>