implement subtype checks
This commit is contained in:
parent
3014213aa7
commit
ccd60fc7bf
3 changed files with 124 additions and 2 deletions
|
@ -6,6 +6,7 @@ pub mod lexer;
|
|||
pub mod parser;
|
||||
pub mod curry;
|
||||
pub mod lnf;
|
||||
pub mod subtype;
|
||||
|
||||
#[cfg(test)]
|
||||
mod test;
|
||||
|
|
51
src/subtype.rs
Normal file
51
src/subtype.rs
Normal file
|
@ -0,0 +1,51 @@
|
|||
use crate::term::TypeTerm;
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
impl TypeTerm {
|
||||
// returns ladder-step of first match and provided representation-type
|
||||
pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<(usize, TypeTerm)> {
|
||||
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, TypeTerm::Ladder(
|
||||
provided_lnf[i..].into_iter().cloned().collect()
|
||||
)))
|
||||
}
|
||||
}
|
||||
|
||||
None
|
||||
}
|
||||
|
||||
pub fn is_syntactic_subtype_of(&self, expected_type: &TypeTerm) -> Result<usize, Option<(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(Some((first_match, first_match+i)))
|
||||
}
|
||||
}
|
||||
|
||||
Ok(first_match)
|
||||
} else {
|
||||
Err(None)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// supertype analogs
|
||||
|
||||
pub fn is_semantic_supertype_of(&self, t: &TypeTerm) -> Option<(usize, TypeTerm)> {
|
||||
t.is_semantic_subtype_of(self)
|
||||
}
|
||||
|
||||
pub fn is_syntactic_supertype_of(&self, t: &TypeTerm) -> Result<usize, Option<(usize, usize)>> {
|
||||
t.is_syntactic_subtype_of(self)
|
||||
}
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
|
@ -1,6 +1,76 @@
|
|||
use crate::dict::TypeDict;
|
||||
|
||||
#[test]
|
||||
fn test_subtype() {
|
||||
// todo
|
||||
fn test_semantic_subtype() {
|
||||
let mut dict = TypeDict::new();
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C").expect("parse error")
|
||||
.is_semantic_subtype_of(
|
||||
&dict.parse("A~B~C").expect("parse errror")
|
||||
),
|
||||
Some((0, dict.parse("A~B~C").expect("parse errror")))
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B1~C1").expect("parse error")
|
||||
.is_semantic_subtype_of(
|
||||
&dict.parse("A~B2~C2").expect("parse errror")
|
||||
),
|
||||
Some((0, dict.parse("A~B1~C1").expect("parse errror")))
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C1").expect("parse error")
|
||||
.is_semantic_subtype_of(
|
||||
&dict.parse("B~C2").expect("parse errror")
|
||||
),
|
||||
Some((1, dict.parse("B~C1").expect("parse errror")))
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn test_syntactic_subtype() {
|
||||
let mut dict = TypeDict::new();
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C").expect("parse error")
|
||||
.is_syntactic_subtype_of(
|
||||
&dict.parse("A~B~C").expect("parse errror")
|
||||
),
|
||||
Ok(0)
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C").expect("parse error")
|
||||
.is_syntactic_subtype_of(
|
||||
&dict.parse("B~C").expect("parse errror")
|
||||
),
|
||||
Ok(1)
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C~D~E").expect("parse error")
|
||||
.is_syntactic_subtype_of(
|
||||
&dict.parse("C~D").expect("parse errror")
|
||||
),
|
||||
Ok(2)
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C~D~E").expect("parse error")
|
||||
.is_syntactic_subtype_of(
|
||||
&dict.parse("C~G").expect("parse errror")
|
||||
),
|
||||
Err(Some((2,3)))
|
||||
);
|
||||
|
||||
assert_eq!(
|
||||
dict.parse("A~B~C~D~E").expect("parse error")
|
||||
.is_syntactic_subtype_of(
|
||||
&dict.parse("G~F~K").expect("parse errror")
|
||||
),
|
||||
Err(None)
|
||||
);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue