rewrite of pnf sugared
This commit is contained in:
parent
2ecbc84233
commit
69ec5ad8bb
GPG key ID:
F96CF119C34B64A6
1 changed files with 177 additions and 97 deletions
|
|
@ -3,6 +3,7 @@ use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
|
|||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm > ) -> Vec< SugaredTypeTerm > {
|
||||
// check for overlap
|
||||
for i in 0 .. upper.len() {
|
||||
if upper[i] == lower[0] {
|
||||
let mut result_ladder = Vec::<SugaredTypeTerm>::new();
|
||||
|
|
@ -12,6 +13,7 @@ pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< Sugare
|
|||
}
|
||||
}
|
||||
|
||||
// no overlap found, just concatenate ladders
|
||||
upper.append(&mut lower);
|
||||
upper
|
||||
}
|
||||
|
|
@ -24,132 +26,210 @@ impl SugaredTypeTerm {
|
|||
/// <Seq <Digit 10>>~<Seq Char>
|
||||
/// ⇒ <Seq <Digit 10>~Char>
|
||||
/// ```
|
||||
pub fn param_normalize(mut self) -> Self {
|
||||
|
||||
pub fn normalize(mut self) -> Self {
|
||||
eprintln!("normalize {:?}", self);
|
||||
match self {
|
||||
SugaredTypeTerm::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) {
|
||||
(SugaredTypeTerm::Spec(bot_args), SugaredTypeTerm::Spec(last_args)) => {
|
||||
if bot_args.len() == last_args.len() {
|
||||
let mut new_rung_params = Vec::new();
|
||||
let mut require_break = false;
|
||||
if rungs.len() == 0 {
|
||||
return SugaredTypeTerm::unit();
|
||||
} else if rungs.len() == 1 {
|
||||
return rungs.pop().unwrap().normalize();
|
||||
}
|
||||
|
||||
if bot_args.len() > 0 {
|
||||
todo!();
|
||||
/*
|
||||
if let Ok(_idx) = last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
|
||||
for i in 0 .. bot_args.len() {
|
||||
let mut new_rungs = Vec::new();
|
||||
let mut r2 = rungs.pop().unwrap().strip();
|
||||
while let Some(r1) = rungs.pop() {
|
||||
let r1 = r1.strip();
|
||||
match (r1.clone(), r2.clone()) {
|
||||
(SugaredTypeTerm::Seq { seq_repr: seq_repr1, items: items1 },
|
||||
SugaredTypeTerm::Seq { seq_repr: seq_repr2, items: items2 })
|
||||
=> {
|
||||
eprintln!("popped two seq {:?} , {:?}", items1, items2);
|
||||
r2 = SugaredTypeTerm::Seq {
|
||||
seq_repr:
|
||||
if seq_repr1.is_some() || seq_repr2.is_some() {
|
||||
let sr1 = if let Some(seq_repr1) = seq_repr1 { *seq_repr1.clone() }
|
||||
else { SugaredTypeTerm::unit() };
|
||||
let sr2 = if let Some(seq_repr2) = seq_repr2 { *seq_repr2 }
|
||||
else { SugaredTypeTerm::unit() };
|
||||
|
||||
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 {
|
||||
SugaredTypeTerm::Ladder(spliced_type_ladder)
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
};
|
||||
|
||||
new_rung_params.push( spliced_type.param_normalize() );
|
||||
}
|
||||
|
||||
} else {
|
||||
new_rung_params.push(
|
||||
SugaredTypeTerm::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 {
|
||||
SugaredTypeTerm::Ladder(spliced_type_ladder)
|
||||
} else {
|
||||
SugaredTypeTerm::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( SugaredTypeTerm::Spec(new_rung_params) );
|
||||
Some(Box::new(
|
||||
if sr1 == sr2 {
|
||||
sr1
|
||||
} else if sr1 == SugaredTypeTerm::unit() {
|
||||
sr2
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ sr1, sr2 ]).normalize()
|
||||
}))
|
||||
} else {
|
||||
rungs.pop();
|
||||
rungs.push(SugaredTypeTerm::Spec(new_rung_params));
|
||||
}
|
||||
None
|
||||
},
|
||||
items:
|
||||
items1.into_iter()
|
||||
.zip(items2.into_iter())
|
||||
.map(|(item1, item2)| {
|
||||
if item1 == item2 {
|
||||
item1
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ item1.clone(), item2 ])
|
||||
}
|
||||
})
|
||||
.collect()
|
||||
};
|
||||
}
|
||||
|
||||
} else {
|
||||
new_rungs.push( SugaredTypeTerm::Spec(bot_args) );
|
||||
}
|
||||
}
|
||||
(bottom, last_buf) => {
|
||||
new_rungs.push( bottom );
|
||||
}
|
||||
(SugaredTypeTerm::Seq { seq_repr, items },
|
||||
SugaredTypeTerm::Spec( mut args )
|
||||
) => {
|
||||
if args.len() == items.len()+1 {
|
||||
r2 = SugaredTypeTerm::Seq {
|
||||
seq_repr: Some(Box::new(SugaredTypeTerm::Ladder(vec![
|
||||
if let Some(seq_repr) = seq_repr {
|
||||
*seq_repr.clone()
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
},
|
||||
args.remove(0)
|
||||
]).normalize())),
|
||||
|
||||
items: items.into_iter()
|
||||
.zip(args.into_iter())
|
||||
.map(|(i1, i2)| {
|
||||
if i1 == i2 {
|
||||
i1
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ i1, i2 ]).normalize()
|
||||
}
|
||||
})
|
||||
.collect()
|
||||
};
|
||||
} else {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
}
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Struct { struct_repr: struct_repr1, members: members1 },
|
||||
SugaredTypeTerm::Struct { struct_repr: struct_repr2, members: members2 }) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Enum { enum_repr: enum_repr1, variants: variants1 },
|
||||
SugaredTypeTerm::Enum { enum_repr: enum_repr2, variants: variants2 }) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Spec(args1), SugaredTypeTerm::Spec(args2)) => {
|
||||
eprintln!("popped two spec {:?} , {:?}", args1, args2);
|
||||
if args1.len() == args2.len() {
|
||||
r2 = SugaredTypeTerm::Spec(
|
||||
args1.into_iter().zip(args2.into_iter())
|
||||
.map(|(a1,a2)|
|
||||
if a1 == SugaredTypeTerm::unit() {
|
||||
a2
|
||||
} else if a1 == a2 {
|
||||
a2
|
||||
} else if a2 == SugaredTypeTerm::unit() {
|
||||
a1
|
||||
} else {
|
||||
SugaredTypeTerm::Ladder(vec![ a1, a2 ]).normalize()
|
||||
})
|
||||
.collect()
|
||||
);
|
||||
} else {
|
||||
new_rungs.push(r2);
|
||||
r2 = r1;
|
||||
}
|
||||
}
|
||||
(SugaredTypeTerm::Univ(args1), SugaredTypeTerm::Univ(args2)) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Func(args1), SugaredTypeTerm::Func(args2)) => {
|
||||
todo!();
|
||||
}
|
||||
(SugaredTypeTerm::Morph(args1), SugaredTypeTerm::Morph(args2)) => {
|
||||
todo!();
|
||||
}
|
||||
|
||||
(SugaredTypeTerm::Ladder(rr1), SugaredTypeTerm::Ladder(rr2)) => {
|
||||
eprintln!("popped two ladders {:?} , {:?}", rr1, rr2);
|
||||
|
||||
if rr1.len() > 0 {
|
||||
let l = splice_ladders(rr1, rr2);
|
||||
eprintln!("splice ladders .. = {:?}",l);
|
||||
r2 = SugaredTypeTerm::Ladder(l).normalize();
|
||||
}
|
||||
}
|
||||
|
||||
(atomic1, SugaredTypeTerm::Ladder(mut rr2)) => {
|
||||
if !atomic1.is_empty() {
|
||||
eprintln!("add head of ladder");
|
||||
if rr2.first() != Some(&atomic1) {
|
||||
rr2.insert(0, atomic1);
|
||||
} else {
|
||||
eprintln!("skip equal head at ladder");
|
||||
}
|
||||
} else {
|
||||
eprintln!("skip empty atomic at head of ladder");
|
||||
}
|
||||
r2 = SugaredTypeTerm::Ladder(rr2).normalize();
|
||||
}
|
||||
|
||||
(atomic1, atomic2) => {
|
||||
eprintln!("popped two atomics {:?} , {:?}", atomic1, atomic2);
|
||||
if atomic1.is_empty() {
|
||||
eprintln!("skip atomic1 (empty)");
|
||||
} else if atomic1 == atomic2 {
|
||||
eprintln!("atomic are equal");
|
||||
if !atomic2.is_empty() {
|
||||
new_rungs.push(atomic2);
|
||||
}
|
||||
r2 = atomic1;
|
||||
} else if atomic2.is_empty() {
|
||||
eprintln!("lol");
|
||||
r2 = atomic1;
|
||||
} else {
|
||||
eprintln!("differnt, take atomic2");
|
||||
new_rungs.push(atomic2);
|
||||
r2 = atomic1;
|
||||
}
|
||||
} else {
|
||||
new_rungs.push( bottom );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if new_rungs.len() > 0 {
|
||||
new_rungs.push(r2);
|
||||
new_rungs.reverse();
|
||||
|
||||
if new_rungs.len() > 1 {
|
||||
SugaredTypeTerm::Ladder(new_rungs)
|
||||
} else if new_rungs.len() == 1 {
|
||||
new_rungs[0].clone()
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
}
|
||||
return SugaredTypeTerm::Ladder(new_rungs);
|
||||
} else {
|
||||
SugaredTypeTerm::unit()
|
||||
return r2;
|
||||
}
|
||||
}
|
||||
|
||||
SugaredTypeTerm::Spec(params) => {
|
||||
SugaredTypeTerm::Spec(
|
||||
params.into_iter()
|
||||
.map(|p| p.param_normalize())
|
||||
.map(|p| p.normalize())
|
||||
.collect())
|
||||
}
|
||||
|
||||
SugaredTypeTerm::Seq { seq_repr, items } => SugaredTypeTerm::Seq {
|
||||
seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.param_normalize())) } else { None },
|
||||
items: items.into_iter().map(|p| p.param_normalize()).collect()
|
||||
seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.normalize())) } else { None },
|
||||
items: items.into_iter().map(|p| p.normalize()).collect()
|
||||
},
|
||||
SugaredTypeTerm::Struct { struct_repr, members } =>SugaredTypeTerm::Struct {
|
||||
struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.param_normalize())) } else { None },
|
||||
SugaredTypeTerm::Struct { struct_repr, members } => SugaredTypeTerm::Struct {
|
||||
struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.normalize())) } else { None },
|
||||
members: members.into_iter()
|
||||
.map(|SugaredStructMember{symbol, ty}|
|
||||
SugaredStructMember{ symbol, ty: ty.param_normalize() })
|
||||
SugaredStructMember{ symbol, ty: ty.normalize() })
|
||||
.collect()
|
||||
},
|
||||
SugaredTypeTerm::Enum{ enum_repr, variants } => SugaredTypeTerm::Enum{
|
||||
enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.param_normalize())) } else { None },
|
||||
SugaredTypeTerm::Enum { enum_repr, variants } => SugaredTypeTerm::Enum{
|
||||
enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.normalize())) } else { None },
|
||||
variants: variants.into_iter()
|
||||
.map(|SugaredEnumVariant{symbol, ty}|
|
||||
SugaredEnumVariant{ symbol, ty: ty.param_normalize() })
|
||||
SugaredEnumVariant{ symbol, ty: ty.normalize() })
|
||||
.collect()
|
||||
},
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue