TypeTerm: type-ladder arguments, variables & char-literals
This commit is contained in:
parent
f1eedad3fe
commit
17b58e6bca
9 changed files with 224 additions and 128 deletions
|
@ -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()
|
||||
]
|
||||
}
|
||||
));
|
||||
|
|
|
@ -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<dyn SingletonView<Item = ListCursor>> {
|
||||
|
|
|
@ -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<TypeTerm>);
|
||||
|
||||
#[derive(Clone, Copy, Hash, PartialEq, Eq)]
|
||||
pub enum MorphismMode {
|
||||
/// Isomorphism
|
||||
|
@ -50,12 +48,12 @@ impl From<MorphismType> 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<MorphismType> for MorphismTypePattern {
|
|||
|
||||
pub struct Context {
|
||||
/// assigns a name to every type
|
||||
type_dict: Arc<RwLock<TypeDict>>,
|
||||
pub type_dict: Arc<RwLock<TypeDict>>,
|
||||
|
||||
/// 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<u64> {
|
||||
match self.get_typeid(tn) {
|
||||
Some(TypeID::Fun(x)) => Some(x),
|
||||
_ => None
|
||||
}
|
||||
}
|
||||
|
||||
pub fn get_var_typeid(&self, tn: &str) -> Option<u64> {
|
||||
match self.get_typeid(tn) {
|
||||
Some(TypeID::Var(x)) => Some(x),
|
||||
_ => None
|
||||
}
|
||||
}
|
||||
|
||||
pub fn type_term_from_str(&self, tn: &str) -> Option<TypeTerm> {
|
||||
self.type_dict.read().unwrap().type_term_from_str(&tn)
|
||||
}
|
||||
|
|
71
nested/src/type_system/dict.rs
Normal file
71
nested/src/type_system/dict.rs
Normal file
|
@ -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<String, TypeID>,
|
||||
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<String> {
|
||||
self.typenames.my.get(tid).cloned()
|
||||
}
|
||||
|
||||
pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
|
||||
self.typenames.mλ.get(tn).cloned()
|
||||
}
|
||||
|
||||
pub fn type_term_from_str(&self, typename: &str) -> Option<TypeTerm> {
|
||||
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)
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
71
nested/src/type_system/ladder.rs
Normal file
71
nested/src/type_system/ladder.rs
Normal file
|
@ -0,0 +1,71 @@
|
|||
use {
|
||||
crate::type_system::{TypeTerm, TypeID},
|
||||
std::collections::HashMap
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
#[derive(Clone, Eq, PartialEq, Hash, Debug)]
|
||||
pub struct TypeLadder(pub Vec<TypeTerm>);
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
impl From<Vec<TypeTerm>> for TypeLadder {
|
||||
fn from(l: Vec<TypeTerm>) -> Self {
|
||||
TypeLadder(l)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<TypeTerm> 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<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)
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_str1(&self, names: &HashMap<TypeID, String>) -> 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
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
|
@ -75,7 +75,7 @@ pub fn init_editor_ctx(parent: Arc<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
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<RwLock<Context>>) -> Arc<RwLock<Context>> {
|
|||
TypeTerm::new(ctx.read().unwrap().get_typeid("Digit").unwrap())
|
||||
.num_arg(radix)
|
||||
.clone()
|
||||
.into()
|
||||
]
|
||||
},
|
||||
depth+1
|
||||
|
|
|
@ -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::*
|
||||
|
|
|
@ -1,66 +1,36 @@
|
|||
use {crate::utils::Bimap, std::collections::HashMap};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
pub type TypeID = u64;
|
||||
|
||||
#[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)
|
||||
}
|
||||
}
|
||||
}
|
||||
use {
|
||||
crate::{
|
||||
type_system::{TypeLadder, TypeID}
|
||||
},
|
||||
std::collections::HashMap
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum TypeTerm {
|
||||
Type { id: TypeID, args: Vec<TypeTerm> },
|
||||
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<TypeLadder>) -> &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<String, u64>) -> Option<Self> {
|
||||
|
||||
pub fn char_arg(&mut self, c: char) -> &mut Self {
|
||||
self.arg(TypeTerm::Char(c))
|
||||
}
|
||||
|
||||
pub fn from_str(s: &str, names: &HashMap<String, TypeID>) -> Option<Self> {
|
||||
let mut term_stack = Vec::<Option<TypeTerm>>::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<u64, String>) -> String {
|
||||
pub fn to_str1(&self, names: &HashMap<TypeID, String>) -> 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<u64, String>) -> String {
|
||||
pub fn to_str(&self, names: &HashMap<TypeID, String>) -> 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<String, u64>,
|
||||
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<String> {
|
||||
self.typenames.my.get(tid).cloned()
|
||||
}
|
||||
|
||||
pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
|
||||
self.typenames.mλ.get(tn).cloned()
|
||||
}
|
||||
|
||||
pub fn type_term_from_str(&self, typename: &str) -> Option<TypeTerm> {
|
||||
TypeTerm::from_str(typename, &self.typenames.mλ)
|
||||
}
|
||||
|
||||
pub fn type_term_to_str(&self, term: &TypeTerm) -> String {
|
||||
term.to_str(&self.typenames.my)
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
Loading…
Reference in a new issue