2024-01-18 19:32:49 +01:00
|
|
|
use {
|
2023-09-08 13:40:06 +02:00
|
|
|
r3vi::{view::{OuterViewPort, singleton::*}, buffer::{singleton::*}},
|
2023-11-12 18:07:20 +01:00
|
|
|
laddertypes::{TypeDict, TypeTerm, TypeID},
|
2022-05-08 23:30:49 +02:00
|
|
|
crate::{
|
2024-01-18 19:32:49 +01:00
|
|
|
repr_tree::{ReprTree, MorphismType, GenericReprTreeMorphism, MorphismBase},
|
2024-01-07 20:04:23 +01:00
|
|
|
edit_tree::EditTree
|
2021-11-19 12:19:52 +01:00
|
|
|
},
|
2021-04-30 03:49:53 +02:00
|
|
|
std::{
|
|
|
|
collections::HashMap,
|
2021-11-19 12:19:52 +01:00
|
|
|
sync::{Arc, RwLock},
|
2021-04-30 03:49:53 +02:00
|
|
|
}
|
2023-01-02 13:18:55 +01:00
|
|
|
};
|
2021-04-30 03:49:53 +02:00
|
|
|
|
|
|
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
|
|
|
|
2023-05-19 11:26:05 +02:00
|
|
|
#[derive(Clone)]
|
2021-05-10 01:57:47 +02:00
|
|
|
pub struct Context {
|
2022-05-08 23:30:49 +02:00
|
|
|
/// assigns a name to every type
|
2023-03-02 03:43:38 +01:00
|
|
|
pub type_dict: Arc<RwLock<TypeDict>>,
|
2022-11-18 00:21:29 +01:00
|
|
|
|
2024-01-18 19:32:49 +01:00
|
|
|
pub morphisms: MorphismBase,
|
|
|
|
|
2023-02-24 18:44:47 +01:00
|
|
|
/// named vertices of the graph
|
2024-01-18 19:32:49 +01:00
|
|
|
nodes: HashMap< String, Arc<RwLock<ReprTree>> >,
|
2022-05-08 23:30:49 +02:00
|
|
|
|
2023-02-17 00:59:07 +01:00
|
|
|
/// todo: beautify
|
2023-02-13 18:39:45 +01:00
|
|
|
/// types that can be edited as lists
|
2024-01-18 19:32:49 +01:00
|
|
|
/// do we really need this?
|
2023-05-19 11:26:05 +02:00
|
|
|
pub list_types: Vec< TypeID >,
|
|
|
|
pub meta_chars: Vec< char >,
|
2022-05-08 23:30:49 +02:00
|
|
|
|
2024-01-17 03:42:47 +01:00
|
|
|
edittree_hook: Arc< dyn Fn(Arc<RwLock<EditTree>>, TypeTerm) + Send +Sync +'static >,
|
|
|
|
|
2022-05-08 23:30:49 +02:00
|
|
|
/// recursion
|
2021-11-19 12:19:52 +01:00
|
|
|
parent: Option<Arc<RwLock<Context>>>,
|
2021-04-30 03:49:53 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
impl Context {
|
2024-01-17 03:42:47 +01:00
|
|
|
pub fn with_parent(
|
|
|
|
parent: Option<Arc<RwLock<Context>>>
|
|
|
|
) -> Self {
|
2021-05-10 01:57:47 +02:00
|
|
|
Context {
|
2022-11-19 01:45:57 +01:00
|
|
|
type_dict: match parent.as_ref() {
|
|
|
|
Some(p) => p.read().unwrap().type_dict.clone(),
|
|
|
|
None => Arc::new(RwLock::new(TypeDict::new()))
|
|
|
|
},
|
2024-01-18 19:32:49 +01:00
|
|
|
morphisms: MorphismBase::new(),
|
2023-02-17 00:59:07 +01:00
|
|
|
nodes: HashMap::new(),
|
2023-02-13 18:39:45 +01:00
|
|
|
list_types: match parent.as_ref() {
|
|
|
|
Some(p) => p.read().unwrap().list_types.clone(),
|
|
|
|
None => Vec::new()
|
|
|
|
},
|
2023-05-19 11:26:05 +02:00
|
|
|
meta_chars: match parent.as_ref() {
|
|
|
|
Some(p) => p.read().unwrap().meta_chars.clone(),
|
|
|
|
None => Vec::new()
|
|
|
|
},
|
2021-11-19 12:19:52 +01:00
|
|
|
parent,
|
2024-01-17 03:42:47 +01:00
|
|
|
|
|
|
|
edittree_hook: Arc::new(|_et, _t| {})
|
2021-05-10 01:57:47 +02:00
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn new() -> Self {
|
|
|
|
Context::with_parent(None)
|
|
|
|
}
|
|
|
|
|
2024-01-17 03:42:47 +01:00
|
|
|
pub fn set_edittree_hook(&mut self, hook: Arc< dyn Fn(Arc<RwLock<EditTree>>, TypeTerm) + Send +Sync +'static >) {
|
|
|
|
self.edittree_hook = hook;
|
|
|
|
}
|
|
|
|
|
2023-02-17 00:59:07 +01:00
|
|
|
pub fn depth(&self) -> usize {
|
|
|
|
if let Some(parent) = self.parent.as_ref() {
|
|
|
|
parent.read().unwrap().depth() + 1
|
|
|
|
} else {
|
|
|
|
0
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2024-01-04 15:39:39 +01:00
|
|
|
pub fn make_repr(ctx: &Arc<RwLock<Self>>, t: &TypeTerm) -> Arc<RwLock<ReprTree>> {
|
|
|
|
let rt = Arc::new(RwLock::new(ReprTree::new( TypeTerm::unit() )));
|
|
|
|
ctx.read().unwrap().morphisms.morph( rt.clone(), t );
|
|
|
|
rt
|
|
|
|
}
|
|
|
|
|
2023-11-12 18:07:20 +01:00
|
|
|
pub fn parse(ctx: &Arc<RwLock<Self>>, s: &str) -> TypeTerm {
|
|
|
|
ctx.read().unwrap().type_term_from_str(s).expect("could not parse type term")
|
|
|
|
}
|
|
|
|
|
2023-08-17 22:48:09 +02:00
|
|
|
pub fn add_typename(&mut self, tn: &str) -> TypeID {
|
|
|
|
self.type_dict.write().unwrap().add_typename(tn.to_string())
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn add_varname(&mut self, vn: &str) -> TypeID {
|
|
|
|
self.type_dict.write().unwrap().add_varname(vn.to_string())
|
2023-02-13 18:39:45 +01:00
|
|
|
}
|
|
|
|
|
2023-09-04 06:17:14 +02:00
|
|
|
pub fn add_synonym(&mut self, new: &str, old: &str) {
|
|
|
|
self.type_dict.write().unwrap().add_synonym(new.to_string(), old.to_string());
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn add_list_typename(&mut self, tn: &str) {
|
|
|
|
let tid = self.add_typename(tn);
|
2023-02-13 18:39:45 +01:00
|
|
|
self.list_types.push( tid );
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn is_list_type(&self, t: &TypeTerm) -> bool {
|
|
|
|
match t {
|
2023-08-12 19:03:14 +02:00
|
|
|
TypeTerm::TypeID(id) => {
|
|
|
|
self.list_types.contains(id)
|
2023-02-13 18:39:45 +01:00
|
|
|
}
|
2023-09-15 15:15:59 +02:00
|
|
|
TypeTerm::Ladder(args) |
|
|
|
|
TypeTerm::App(args) => {
|
|
|
|
if args.len() > 0 {
|
|
|
|
if self.is_list_type(&args[0]) {
|
|
|
|
true
|
|
|
|
} else {
|
|
|
|
false
|
|
|
|
}
|
|
|
|
} else {
|
|
|
|
false
|
|
|
|
}
|
|
|
|
}
|
2023-02-13 18:39:45 +01:00
|
|
|
_ => false
|
|
|
|
}
|
2021-05-10 01:57:47 +02:00
|
|
|
}
|
|
|
|
|
2022-12-19 11:26:07 +01:00
|
|
|
pub fn get_typeid(&self, tn: &str) -> Option<TypeID> {
|
|
|
|
self.type_dict.read().unwrap().get_typeid(&tn.into())
|
|
|
|
}
|
|
|
|
|
2023-03-02 03:43:38 +01:00
|
|
|
pub fn get_fun_typeid(&self, tn: &str) -> Option<u64> {
|
|
|
|
match self.get_typeid(tn) {
|
|
|
|
Some(TypeID::Fun(x)) => Some(x),
|
|
|
|
_ => None
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2023-08-12 19:03:14 +02:00
|
|
|
pub fn get_typename(&self, tid: &TypeID) -> Option<String> {
|
|
|
|
self.type_dict.read().unwrap().get_typename(tid)
|
|
|
|
}
|
|
|
|
|
2023-03-02 03:43:38 +01:00
|
|
|
pub fn get_var_typeid(&self, tn: &str) -> Option<u64> {
|
|
|
|
match self.get_typeid(tn) {
|
|
|
|
Some(TypeID::Var(x)) => Some(x),
|
|
|
|
_ => None
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
2023-11-12 18:07:20 +01:00
|
|
|
pub fn type_term_from_str(&self, tn: &str) -> Result<TypeTerm, laddertypes::parser::ParseError> {
|
|
|
|
self.type_dict.write().unwrap().parse(&tn)
|
2021-05-10 01:57:47 +02:00
|
|
|
}
|
2022-12-18 01:20:17 +01:00
|
|
|
|
2022-05-08 23:30:49 +02:00
|
|
|
pub fn type_term_to_str(&self, t: &TypeTerm) -> String {
|
2023-11-12 18:07:20 +01:00
|
|
|
self.type_dict.read().unwrap().unparse(&t)
|
2022-05-08 23:30:49 +02:00
|
|
|
}
|
2021-05-10 01:57:47 +02:00
|
|
|
/// adds an object without any representations
|
2023-02-17 00:59:07 +01:00
|
|
|
pub fn add_obj(ctx: Arc<RwLock<Context>>, name: String, typename: &str) {
|
|
|
|
let type_tag = ctx.read().unwrap()
|
2023-11-12 18:07:20 +01:00
|
|
|
.type_dict.write().unwrap()
|
|
|
|
.parse(typename).unwrap();
|
2021-05-10 01:57:47 +02:00
|
|
|
|
2024-01-18 19:32:49 +01:00
|
|
|
/*
|
2023-09-08 13:40:06 +02:00
|
|
|
if let Some(node) = Context::make_node(&ctx, type_tag, SingletonBuffer::new(0).get_port()) {
|
2023-02-17 00:59:07 +01:00
|
|
|
ctx.write().unwrap().nodes.insert(name, node);
|
|
|
|
}
|
2024-01-18 19:32:49 +01:00
|
|
|
*/
|
2021-04-30 03:49:53 +02:00
|
|
|
}
|
|
|
|
|
2024-01-18 19:32:49 +01:00
|
|
|
pub fn get_obj(&self, name: &String) -> Option< Arc<RwLock<ReprTree>> > {
|
2023-02-17 00:59:07 +01:00
|
|
|
if let Some(obj) = self.nodes.get(name) {
|
2021-05-10 01:57:47 +02:00
|
|
|
Some(obj.clone())
|
|
|
|
} else if let Some(parent) = self.parent.as_ref() {
|
|
|
|
parent.read().unwrap().get_obj(name)
|
|
|
|
} else {
|
|
|
|
None
|
2021-04-30 03:49:53 +02:00
|
|
|
}
|
|
|
|
}
|
2024-01-17 03:42:47 +01:00
|
|
|
|
|
|
|
pub fn setup_edittree(
|
|
|
|
&self,
|
|
|
|
rt: Arc<RwLock<ReprTree>>,
|
|
|
|
depth: OuterViewPort<dyn SingletonView<Item = usize>>
|
|
|
|
) -> Arc<RwLock<EditTree>> {
|
|
|
|
let ladder = TypeTerm::Ladder(vec![
|
|
|
|
rt.read().unwrap().get_type().clone(),
|
|
|
|
self.type_term_from_str("EditTree").expect("")
|
|
|
|
]);
|
|
|
|
|
|
|
|
self.morphisms.morph(
|
|
|
|
rt.clone(),
|
|
|
|
&ladder
|
|
|
|
);
|
|
|
|
|
|
|
|
let new_edittree = rt
|
|
|
|
.read().unwrap()
|
|
|
|
.descend(
|
|
|
|
self.type_term_from_str("EditTree").expect("")
|
|
|
|
).unwrap()
|
|
|
|
.read().unwrap()
|
|
|
|
.get_view::<dyn SingletonView<Item = Arc<RwLock<EditTree>> >>()
|
|
|
|
.unwrap()
|
|
|
|
.get();
|
|
|
|
|
|
|
|
(*self.edittree_hook)( new_edittree.clone(), rt.read().unwrap().get_type().clone() );
|
|
|
|
|
|
|
|
new_edittree
|
|
|
|
}
|
2021-04-30 03:49:53 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>
|
2023-08-21 15:49:07 +02:00
|
|
|
|