syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Compare commits

base: syntaxAlchemist:dev
Branches Tags
syntaxAlchemist:dev
syntaxAlchemist:topic-morphism-base
syntaxAlchemist:topic-unification
syntaxAlchemist:topic-sugar-wip
syntaxAlchemist:topic-semantic-subtype
syntaxAlchemist:topic-marco
..
compare: syntaxAlchemist:topic-semantic-subtype
Branches Tags
syntaxAlchemist:topic-morphism-base
syntaxAlchemist:topic-unification
syntaxAlchemist:dev
syntaxAlchemist:topic-sugar-wip
syntaxAlchemist:topic-semantic-subtype
syntaxAlchemist:topic-marco

1 commit
dev ... topic-sema

Author SHA1 Message Date
Michael Sippel
3b85bd7621
add find_semantic_subtype_matches() as potential alternative to is_semantic_subtype_of() 2024-08-05 00:11:58 +02:00
9 changed files with 126 additions and 383 deletions
Show stats Expand all files Collapse all files

5
Cargo.toml
View file

@ -4,8 +4,3 @@ edition = "2018"
name = "laddertypes"
version = "0.1.0"
[dependencies]
tiny-ansi = { version = "0.1.0", optional = true }
[features]
pretty = ["dep:tiny-ansi"]

6
src/dict.rs
View file

@ -2,7 +2,7 @@ use crate::bimap::Bimap;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
#[derive(Eq, PartialEq, Hash, Clone, Copy, Debug)]
#[derive(Eq, PartialEq, Hash, Clone, Debug)]
pub enum TypeID {
Fun(u64),
Var(u64)
@ -54,10 +54,6 @@ impl TypeDict {
pub fn get_typeid(&self, tn: &String) -> Option<TypeID> {
self.typenames.mλ.get(tn).cloned()
}
pub fn get_varname(&self, var_id: u64) -> Option<String> {
self.typenames.my.get(&TypeID::Var(var_id)).cloned()
}
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>

8
src/lib.rs
View file

@ -5,7 +5,6 @@ pub mod term;
pub mod lexer;
pub mod parser;
pub mod unparser;
pub mod sugar;
pub mod curry;
pub mod lnf;
pub mod pnf;
@ -15,12 +14,9 @@ pub mod unification;
#[cfg(test)]
mod test;
#[cfg(feature = "pretty")]
mod pretty;
pub use {
dict::*,
term::*,
sugar::*,
unification::*,
unification::*
};

177
src/pnf.rs
View file

@ -2,20 +2,6 @@ use crate::term::TypeTerm;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
pub fn splice_ladders( mut upper: Vec< TypeTerm >, mut lower: Vec< TypeTerm > ) -> Vec< TypeTerm > {
for i in 0 .. upper.len() {
if upper[i] == lower[0] {
let mut result_ladder = Vec::<TypeTerm>::new();
result_ladder.append(&mut upper[0..i].iter().cloned().collect());
result_ladder.append(&mut lower);
return result_ladder;
}
}
upper.append(&mut lower);
upper
}
impl TypeTerm {
/// transmute type into Parameter-Normal-Form (PNF)
///
@ -24,99 +10,88 @@ impl TypeTerm {
/// <Seq <Digit 10>>~<Seq Char>
/// ⇒ <Seq <Digit 10>~Char>
/// ```
pub fn param_normalize(mut self) -> Self {
pub fn param_normalize(self) -> Self {
match self {
TypeTerm::Ladder(mut rungs) => {
if rungs.len() > 0 {
let mut new_rungs = Vec::new();
while let Some(bottom) = rungs.pop() {
if let Some(last_but) = rungs.last_mut() {
match (bottom, last_but) {
(TypeTerm::App(bot_args), TypeTerm::App(last_args)) => {
if bot_args.len() == last_args.len() {
let mut new_rung_params = Vec::new();
let mut require_break = false;
if bot_args.len() > 0 {
if let Ok(_idx) = last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
for i in 0 .. bot_args.len() {
let spliced_type_ladder = splice_ladders(
last_args[i].clone().get_lnf_vec(),
bot_args[i].clone().get_lnf_vec()
);
let spliced_type =
if spliced_type_ladder.len() == 1 {
spliced_type_ladder[0].clone()
} else if spliced_type_ladder.len() > 1 {
TypeTerm::Ladder(spliced_type_ladder)
} else {
TypeTerm::unit()
};
new_rung_params.push( spliced_type.param_normalize() );
}
} else {
new_rung_params.push(
TypeTerm::Ladder(vec![
last_args[0].clone(),
bot_args[0].clone()
]).normalize()
);
for i in 1 .. bot_args.len() {
if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
let spliced_type_ladder = splice_ladders(
last_args[i].clone().get_lnf_vec(),
bot_args[i].clone().get_lnf_vec()
);
let spliced_type =
if spliced_type_ladder.len() == 1 {
spliced_type_ladder[0].clone()
} else if spliced_type_ladder.len() > 1 {
TypeTerm::Ladder(spliced_type_ladder)
} else {
TypeTerm::unit()
};
new_rung_params.push( spliced_type.param_normalize() );
} else {
new_rung_params.push( bot_args[i].clone() );
require_break = true;
}
}
}
}
if require_break {
new_rungs.push( TypeTerm::App(new_rung_params) );
} else {
rungs.pop();
rungs.push(TypeTerm::App(new_rung_params));
}
} else {
new_rungs.push( TypeTerm::App(bot_args) );
}
}
(bottom, last_buf) => {
new_rungs.push( bottom );
}
}
} else {
new_rungs.push( bottom );
}
// normalize all rungs separately
for r in rungs.iter_mut() {
*r = r.clone().param_normalize();
}
new_rungs.reverse();
// take top-rung
match rungs.remove(0) {
TypeTerm::App(params_top) => {
let mut params_ladders = Vec::new();
let mut tail : Vec<TypeTerm> = Vec::new();
if new_rungs.len() > 1 {
TypeTerm::Ladder(new_rungs)
} else if new_rungs.len() == 1 {
new_rungs[0].clone()
} else {
TypeTerm::unit()
// append all other rungs to ladders inside
// the application
for p in params_top {
params_ladders.push(vec![ p ]);
}
for r in rungs {
match r {
TypeTerm::App(mut params_rung) => {
if params_rung.len() > 0 {
let mut first_param = params_rung.remove(0);
if first_param == params_ladders[0][0] {
for (l, p) in params_ladders.iter_mut().skip(1).zip(params_rung) {
l.push(p.param_normalize());
}
} else {
params_rung.insert(0, first_param);
tail.push(TypeTerm::App(params_rung));
}
}
}
TypeTerm::Ladder(mut rs) => {
for r in rs {
tail.push(r.param_normalize());
}
}
atomic => {
tail.push(atomic);
}
}
}
let head = TypeTerm::App(
params_ladders.into_iter()
.map(
|mut l| {
l.dedup();
match l.len() {
0 => TypeTerm::unit(),
1 => l.remove(0),
_ => TypeTerm::Ladder(l).param_normalize()
}
}
)
.collect()
);
if tail.len() > 0 {
tail.insert(0, head);
TypeTerm::Ladder(tail)
} else {
head
}
}
TypeTerm::Ladder(mut r) => {
r.append(&mut rungs);
TypeTerm::Ladder(r)
}
atomic => {
rungs.insert(0, atomic);
TypeTerm::Ladder(rungs)
}
}
} else {
TypeTerm::unit()

148
src/pretty.rs
View file

@ -1,148 +0,0 @@
use {
crate::TypeDict,
crate::sugar::SugaredTypeTerm,
tiny_ansi::TinyAnsi
};
impl SugaredTypeTerm {
pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
let indent_width = 4;
match self {
SugaredTypeTerm::TypeID(id) => {
format!("{}", dict.get_typename(id).unwrap_or("??".bright_red())).bright_blue()
},
SugaredTypeTerm::Num(n) => {
format!("{}", n).bright_cyan()
}
SugaredTypeTerm::Char(c) => {
format!("'{}'", c)
}
SugaredTypeTerm::Univ(t) => {
format!("{} {} . {}",
"∀".yellow().bold(),
dict.get_varname(0).unwrap_or("??".into()).bright_blue(),
t.pretty(dict,indent)
)
}
SugaredTypeTerm::Spec(args) => {
let mut s = String::new();
s.push_str(&"<".yellow().bold());
for i in 0..args.len() {
let arg = &args[i];
if i > 0 {
s.push(' ');
}
s.push_str( &arg.pretty(dict,indent+1) );
}
s.push_str(&">".yellow().bold());
s
}
SugaredTypeTerm::Struct(args) => {
let mut s = String::new();
s.push_str(&"{".yellow().bold());
for arg in args {
s.push('\n');
for x in 0..(indent+1)*indent_width {
s.push(' ');
}
s.push_str(&arg.pretty(dict, indent + 1));
s.push_str(&";\n".bright_yellow());
}
s.push('\n');
for x in 0..indent*indent_width {
s.push(' ');
}
s.push_str(&"}".yellow().bold());
s
}
SugaredTypeTerm::Enum(args) => {
let mut s = String::new();
s.push_str(&"(".yellow().bold());
for i in 0..args.len() {
let arg = &args[i];
s.push('\n');
for x in 0..(indent+1)*indent_width {
s.push(' ');
}
if i > 0 {
s.push_str(&"| ".yellow().bold());
}
s.push_str(&arg.pretty(dict, indent + 1));
}
s.push('\n');
for x in 0..indent*indent_width {
s.push(' ');
}
s.push_str(&")".yellow().bold());
s
}
SugaredTypeTerm::Seq(args) => {
let mut s = String::new();
s.push_str(&"[ ".yellow().bold());
for i in 0..args.len() {
let arg = &args[i];
if i > 0 {
s.push(' ');
}
s.push_str(&arg.pretty(dict, indent+1));
}
s.push_str(&" ]".yellow().bold());
s
}
SugaredTypeTerm::Morph(args) => {
let mut s = String::new();
for arg in args {
s.push_str(&" ~~morph~~> ".bright_yellow());
s.push_str(&arg.pretty(dict, indent));
}
s
}
SugaredTypeTerm::Func(args) => {
let mut s = String::new();
for i in 0..args.len() {
let arg = &args[i];
if i > 0{
s.push('\n');
for x in 0..(indent*indent_width) {
s.push(' ');
}
s.push_str(&"--> ".bright_yellow());
} else {
// s.push_str(" ");
}
s.push_str(&arg.pretty(dict, indent));
}
s
}
SugaredTypeTerm::Ladder(rungs) => {
let mut s = String::new();
for i in 0..rungs.len() {
let rung = &rungs[i];
if i > 0{
s.push('\n');
for x in 0..(indent*indent_width) {
s.push(' ');
}
s.push_str(&"~ ".yellow());
}
s.push_str(&rung.pretty(dict, indent));
}
s
}
}
}
}

44
src/subtype.rs
View file

@ -2,7 +2,49 @@ use crate::term::TypeTerm;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
impl TypeTerm {
impl TypeTerm {
pub fn find_semantic_subtype_matches(&self, expected_type: &TypeTerm)
-> Option<(TypeTerm, TypeTerm, 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] {
// found first match.
// now find first mismatch.
for j in i..usize::min(provided_lnf.len(), i+expected_lnf.len()) {
if provided_lnf[j] != expected_lnf[ j-i ] {
eprintln!("found match at {}, mismatch at {}", i, j);
let syntactic_subladder = TypeTerm::Ladder( provided_lnf[ 0 .. j ].into_iter().cloned().collect() );
let provided_reprladder = TypeTerm::Ladder( provided_lnf[ j .. ].into_iter().cloned().collect() );
let expected_reprladder = TypeTerm::Ladder( expected_lnf[ j-i .. ].into_iter().cloned().collect() );
return Some((syntactic_subladder, provided_reprladder, expected_reprladder));
}
}
eprintln!("only syntactic subtype");
// syntactic subtype
let n = {
if provided_lnf.len() + i < expected_lnf.len() {
1
} else {
2
}
};
let syntactic_subladder = TypeTerm::Ladder( provided_lnf[ 0 .. provided_lnf.len()-1 ].into_iter().cloned().collect() );
let provided_reprladder = TypeTerm::Ladder( provided_lnf[ provided_lnf.len()-n .. ].into_iter().cloned().collect() );
let expected_reprladder = TypeTerm::Ladder( expected_lnf[ provided_lnf.len()-n-i .. ].into_iter().cloned().collect() );
return Some((syntactic_subladder, provided_reprladder, expected_reprladder));
}
}
None
}
// 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();

95
src/sugar.rs
View file

@ -1,95 +0,0 @@
use {
crate::{TypeTerm, TypeID}
};
pub enum SugaredTypeTerm {
TypeID(TypeID),
Num(i64),
Char(char),
Univ(Box< SugaredTypeTerm >),
Spec(Vec< SugaredTypeTerm >),
Func(Vec< SugaredTypeTerm >),
Morph(Vec< SugaredTypeTerm >),
Ladder(Vec< SugaredTypeTerm >),
Struct(Vec< SugaredTypeTerm >),
Enum(Vec< SugaredTypeTerm >),
Seq(Vec< SugaredTypeTerm >)
}
impl TypeTerm {
pub fn sugar(self: TypeTerm, dict: &mut crate::TypeDict) -> SugaredTypeTerm {
match self {
TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id),
TypeTerm::Num(n) => SugaredTypeTerm::Num(n),
TypeTerm::Char(c) => SugaredTypeTerm::Char(c),
TypeTerm::App(args) => if let Some(first) = args.first() {
if first == &dict.parse("Func").unwrap() {
SugaredTypeTerm::Func( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Morph").unwrap() {
SugaredTypeTerm::Morph( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Struct").unwrap() {
SugaredTypeTerm::Struct( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Enum").unwrap() {
SugaredTypeTerm::Enum( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Seq").unwrap() {
SugaredTypeTerm::Seq( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Spec").unwrap() {
SugaredTypeTerm::Spec( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Univ").unwrap() {
SugaredTypeTerm::Univ(Box::new(
SugaredTypeTerm::Spec(
args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect()
)
))
}
else {
SugaredTypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
}
} else {
SugaredTypeTerm::Spec(args.into_iter().map(|t| t.sugar(dict)).collect())
},
TypeTerm::Ladder(rungs) =>
SugaredTypeTerm::Ladder(rungs.into_iter().map(|t| t.sugar(dict)).collect())
}
}
}
impl SugaredTypeTerm {
pub fn desugar(self, dict: &mut crate::TypeDict) -> TypeTerm {
match self {
SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
SugaredTypeTerm::Num(n) => TypeTerm::Num(n),
SugaredTypeTerm::Char(c) => TypeTerm::Char(c),
SugaredTypeTerm::Univ(t) => t.desugar(dict),
SugaredTypeTerm::Spec(ts) => TypeTerm::App(ts.into_iter().map(|t| t.desugar(dict)).collect()),
SugaredTypeTerm::Ladder(ts) => TypeTerm::Ladder(ts.into_iter().map(|t|t.desugar(dict)).collect()),
SugaredTypeTerm::Func(ts) => TypeTerm::App(
std::iter::once( dict.parse("Func").unwrap() ).chain(
ts.into_iter().map(|t| t.desugar(dict))
).collect()),
SugaredTypeTerm::Morph(ts) => TypeTerm::App(
std::iter::once( dict.parse("Morph").unwrap() ).chain(
ts.into_iter().map(|t| t.desugar(dict))
).collect()),
SugaredTypeTerm::Struct(ts) => TypeTerm::App(
std::iter::once( dict.parse("Struct").unwrap() ).chain(
ts.into_iter().map(|t| t.desugar(dict))
).collect()),
SugaredTypeTerm::Enum(ts) => TypeTerm::App(
std::iter::once( dict.parse("Enum").unwrap() ).chain(
ts.into_iter().map(|t| t.desugar(dict))
).collect()),
SugaredTypeTerm::Seq(ts) => TypeTerm::App(
std::iter::once( dict.parse("Seq").unwrap() ).chain(
ts.into_iter().map(|t| t.desugar(dict))
).collect()),
}
}
}

2
src/term.rs
View file

@ -57,7 +57,7 @@ impl TypeTerm {
pub fn repr_as(&mut self, t: impl Into<TypeTerm>) -> &mut Self {
match self {
TypeTerm::Ladder(rungs) => {
rungs.push(t.into());
rungs.push(t.into());
}
_ => {

24
src/test/pnf.rs
View file

@ -19,40 +19,22 @@ fn test_param_normalize() {
dict.parse("<A B>~<A C>").expect("parse error").param_normalize(),
);
assert_eq!(
dict.parse("<A~Y B>").expect("parse error"),
dict.parse("<A B>~<Y B>").expect("parse error").param_normalize(),
);
assert_eq!(
dict.parse("<A B~C D~E>").expect("parse error"),
dict.parse("<A B D>~<A C D>~<A C E>").expect("parse errror").param_normalize(),
);
assert_eq!(
dict.parse("<A~X B~C D~E>").expect("parse error"),
dict.parse("<A B D>~<A B~C E>~<X C E>").expect("parse errror").param_normalize(),
);
assert_eq!(
dict.parse("<Seq <Digit 10>~Char>").expect("parse error"),
dict.parse("<Seq <Digit 10>>~<Seq Char>").expect("parse errror").param_normalize(),
);
assert_eq!(
dict.parse("<Seq Char> ~ <<ValueDelim '\\0'> Char> ~ <<ValueDelim '\\0'> Ascii~x86.UInt8>").expect("parse error").param_normalize(),
dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
);
assert_eq!(
dict.parse("<Seq Char~Ascii> ~ <<ValueDelim '\\0'> Char~Ascii> ~ <<ValueDelim '\\0'> x86.UInt8>").expect("parse error").param_normalize(),
dict.parse("<Seq~<ValueDelim '\\0'> Char~Ascii~x86.UInt8>").expect("parse error")
);
assert_eq!(
dict.parse("<A~Y <B C~D~E> F H H>").expect("parse error"),
dict.parse("<A <B C~D~E> F~G H H>").expect("parse error"),
dict.parse("<A <B C> F H H>
~<A <B D> F H H>
~<A~Y <B E> F H H>").expect("parse errror")
~<A <B E> F H H>
~<A <B E> G H H>").expect("parse errror")
.param_normalize(),
);
}