submodules for term & morphism_graph
This commit is contained in:
parent
6ee2e447d4
commit
314f2141d8
15 changed files with 26 additions and 96 deletions
18
src/lib.rs
18
src/lib.rs
|
@ -2,32 +2,18 @@
|
|||
#![allow(confusable_idents)]
|
||||
#![allow(non_snake_case)]
|
||||
|
||||
pub mod lexer;
|
||||
pub mod parser; // todo sugared variant
|
||||
pub mod curry; // todo: sugared variant
|
||||
//pub mod subtype; // deprecated
|
||||
pub mod unparser;
|
||||
pub mod desugared_term; // deprecated
|
||||
pub mod term;
|
||||
pub mod pnf;
|
||||
pub mod context;
|
||||
pub mod constraint_system;
|
||||
pub mod morphism;
|
||||
pub mod morphism_base;
|
||||
pub mod morphism_path;
|
||||
pub mod morphism_graph;
|
||||
|
||||
#[cfg(test)]
|
||||
mod test;
|
||||
|
||||
#[cfg(feature = "pretty")]
|
||||
mod pretty;
|
||||
|
||||
pub use {
|
||||
context::*,
|
||||
desugared_term::*,
|
||||
term::*,
|
||||
constraint_system::*,
|
||||
morphism::*,
|
||||
morphism_base::*,
|
||||
morphism_path::*,
|
||||
morphism_graph::*,
|
||||
};
|
||||
|
|
|
@ -1,3 +1,9 @@
|
|||
pub mod morphism_base;
|
||||
pub mod morphism_path;
|
||||
|
||||
pub use morphism_base::*;
|
||||
pub use morphism_path::*;
|
||||
|
||||
use {
|
||||
crate::{
|
||||
constraint_system::ConstraintSystem, substitution::Substitution, term::{StructMember, TypeTerm},
|
|
@ -1,7 +1,7 @@
|
|||
use {
|
||||
crate::{
|
||||
morphism_path::{ShortestPathProblem},
|
||||
morphism::{MorphismInstance, Morphism, MorphismType},
|
||||
morphism_graph::{MorphismInstance, Morphism, MorphismType},
|
||||
TypeTerm, StructMember, TypeDict
|
||||
}, std::io::{Write}
|
||||
};
|
|
@ -1,6 +1,8 @@
|
|||
use {
|
||||
crate::{
|
||||
morphism::{Morphism, MorphismInstance, MorphismType}, morphism_base::MorphismBase, term::*, HashMapSubst
|
||||
morphism_graph::{Morphism, MorphismInstance, MorphismType, MorphismBase},
|
||||
term::*,
|
||||
HashMapSubst
|
||||
}
|
||||
};
|
||||
|
|
@ -1,76 +0,0 @@
|
|||
use crate::term::DesugaredTypeTerm;
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
impl DesugaredTypeTerm {
|
||||
// returns ladder-step of first match and provided representation-type
|
||||
pub fn is_semantic_subtype_of(&self, expected_type: &DesugaredTypeTerm) -> Option<(usize, DesugaredTypeTerm)> {
|
||||
let provided_lnf = self.clone().get_lnf_vec();
|
||||
let expected_lnf = expected_type.clone().get_lnf_vec();
|
||||
|
||||
for i in 0..provided_lnf.len() {
|
||||
if provided_lnf[i] == expected_lnf[0] {
|
||||
return Some((i, DesugaredTypeTerm::Ladder(
|
||||
provided_lnf[i..].into_iter().cloned().collect()
|
||||
)))
|
||||
}
|
||||
}
|
||||
|
||||
None
|
||||
}
|
||||
|
||||
pub fn is_syntactic_subtype_of(&self, expected_type: &DesugaredTypeTerm) -> Result<usize, (usize, usize)> {
|
||||
if let Some((first_match, provided_type)) = self.is_semantic_subtype_of( expected_type ) {
|
||||
let provided_lnf = provided_type.get_lnf_vec();
|
||||
let expected_lnf = expected_type.clone().get_lnf_vec();
|
||||
|
||||
for i in 0 .. usize::min( provided_lnf.len(), expected_lnf.len() ) {
|
||||
if provided_lnf[i] != expected_lnf[i] {
|
||||
return Err((first_match, first_match+i))
|
||||
}
|
||||
}
|
||||
|
||||
Ok(first_match)
|
||||
} else {
|
||||
Err((0,0))
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// supertype analogs
|
||||
|
||||
pub fn is_semantic_supertype_of(&self, t: &DesugaredTypeTerm) -> Option<(usize, DesugaredTypeTerm)> {
|
||||
t.is_semantic_subtype_of(self)
|
||||
}
|
||||
|
||||
pub fn is_syntactic_supertype_of(&self, t: &DesugaredTypeTerm) -> Result<usize, (usize, usize)> {
|
||||
t.is_syntactic_subtype_of(self)
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
use crate::sugar::*;
|
||||
|
||||
impl TypeTerm {
|
||||
pub fn is_compatible(&self, supertype: TypeTerm) -> bool {
|
||||
match (self, supertype) {
|
||||
(TypeTerm::TypeID(idl), TypeTerm::TypeID(idr)) => {
|
||||
if *idl == idr {
|
||||
true
|
||||
} else {
|
||||
false
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
(TypeTerm::Ladder(l_rungs), TypeTerm::Ladder(r_rungs)) => {
|
||||
false
|
||||
}
|
||||
|
||||
_ => {
|
||||
false
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
|
@ -1,3 +1,14 @@
|
|||
pub mod lexer;
|
||||
pub mod parser; // todo sugared variant
|
||||
pub mod curry; // todo: sugared variant
|
||||
pub mod unparser;
|
||||
pub mod desugared_term; // deprecated
|
||||
pub mod pnf;
|
||||
|
||||
#[cfg(feature = "pretty")]
|
||||
mod pretty;
|
||||
|
||||
|
||||
use {
|
||||
crate::{
|
||||
parser::ParseLadderType,
|
||||
|
@ -9,6 +20,7 @@ use {
|
|||
std::{ops::Deref}
|
||||
};
|
||||
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Debug)]
|
||||
pub enum VariableConstraint {
|
||||
UnconstrainedType, // <<- add TypeKind here ?
|
|
@ -4,5 +4,5 @@ pub mod parser;
|
|||
pub mod curry;
|
||||
pub mod pnf;
|
||||
pub mod context;
|
||||
pub mod morphism;
|
||||
pub mod constraint_system;
|
||||
pub mod morphism_graph;
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
use {
|
||||
crate::{dict::*, morphism::{Morphism, MorphismInstance, MorphismType}, morphism_base::MorphismBase, morphism_path::ShortestPathProblem, parser::*, HashMapSubst, TypeTerm
|
||||
crate::{dict::*, morphism_graph::{Morphism, MorphismInstance, MorphismType}, morphism_base::MorphismBase, morphism_path::ShortestPathProblem, parser::*, HashMapSubst, TypeTerm
|
||||
},
|
||||
std::collections::HashMap
|
||||
};
|
Loading…
Add table
Add a link
Reference in a new issue