split constraint system into files
This commit is contained in:
parent
a1dd6a5121
commit
17ba81c817
GPG key ID:
F96CF119C34B64A6
6 changed files with 399 additions and 366 deletions
src
145
src/constraint_system/eval_eq.rs
Normal file
145
src/constraint_system/eval_eq.rs
Normal file
|
|
@ -0,0 +1,145 @@
|
|||
use {
|
||||
crate::{
|
||||
dict::*, term::TypeTerm, EnumVariant, StructMember,
|
||||
ConstraintSystem, ConstraintPair, ConstraintError
|
||||
}
|
||||
};
|
||||
|
||||
impl ConstraintSystem {
|
||||
|
||||
|
||||
pub fn eval_equation(&mut self, unification_pair: ConstraintPair) -> Result<(), ConstraintError> {
|
||||
match (&unification_pair.lhs, &unification_pair.rhs) {
|
||||
(TypeTerm::TypeID(TypeID::Var(varid)), t) |
|
||||
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
|
||||
if ! t.contains_var( *varid ) {
|
||||
self.σ.insert(TypeID::Var(*varid), t.clone());
|
||||
self.reapply_subst();
|
||||
Ok(())
|
||||
} else if t == &TypeTerm::TypeID(TypeID::Var(*varid)) {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
|
||||
}
|
||||
}
|
||||
|
||||
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
|
||||
if a1 == a2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
|
||||
}
|
||||
(TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
|
||||
if n1 == n2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
|
||||
}
|
||||
(TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
|
||||
if c1 == c2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
|
||||
}
|
||||
|
||||
(TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
|
||||
(TypeTerm::Spec(a1), TypeTerm::Spec(a2)) => {
|
||||
if a1.len() == a2.len() {
|
||||
for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push(
|
||||
ConstraintPair {
|
||||
lhs: x,
|
||||
rhs: y,
|
||||
addr: new_addr
|
||||
});
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
(TypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
|
||||
TypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
|
||||
=> {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(0);
|
||||
|
||||
if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
|
||||
if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
|
||||
let _seq_repr_ψ = self.eval_equation(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
|
||||
} else {
|
||||
return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if lhs_items.len() == rhs_items.len() {
|
||||
for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
|
||||
{
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
(TypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
|
||||
TypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
|
||||
=> {
|
||||
let new_addr = unification_pair.addr.clone();
|
||||
if let Some(rhs_struct_repr) = rhs_struct_repr.as_ref() {
|
||||
if let Some(lhs_struct_repr) = lhs_struct_repr.as_ref() {
|
||||
let _struct_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_struct_repr.clone(), rhs: *rhs_struct_repr.clone() })?;
|
||||
} else {
|
||||
return Err(ConstraintError{ addr: new_addr.clone(), t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
if lhs_members.len() == rhs_members.len() {
|
||||
for (i,
|
||||
(StructMember{ symbol: lhs_symbol, ty: lhs_ty},
|
||||
StructMember{ symbol: rhs_symbol, ty: rhs_ty })
|
||||
) in
|
||||
lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
|
||||
{
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
(TypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
|
||||
TypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
|
||||
=> {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
if let Some(rhs_enum_repr) = rhs_enum_repr.as_ref() {
|
||||
if let Some(lhs_enum_repr) = lhs_enum_repr.as_ref() {
|
||||
let _enum_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_enum_repr.clone(), rhs: *rhs_enum_repr.clone() })?;
|
||||
} else {
|
||||
return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if lhs_variants.len() == rhs_variants.len() {
|
||||
for (i,
|
||||
(EnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
|
||||
EnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
|
||||
) in
|
||||
lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
|
||||
{
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
_ => Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
0
src/constraint_system/eval_parallel.rs
Normal file
0
src/constraint_system/eval_parallel.rs
Normal file
|
|
@ -1,299 +1,11 @@
|
|||
use {
|
||||
crate::{dict::*, term::TypeTerm, desugared_term::*, EnumVariant, StructMember, Substitution}, std::collections::HashMap
|
||||
crate::{
|
||||
dict::*, term::TypeTerm, EnumVariant, StructMember,
|
||||
ConstraintSystem, ConstraintPair, ConstraintError
|
||||
}
|
||||
};
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, Eq, PartialEq, Debug)]
|
||||
pub struct ConstraintError {
|
||||
pub addr: Vec<usize>,
|
||||
pub t1: TypeTerm,
|
||||
pub t2: TypeTerm
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct ConstraintPair {
|
||||
pub addr: Vec<usize>,
|
||||
pub lhs: TypeTerm,
|
||||
pub rhs: TypeTerm,
|
||||
}
|
||||
|
||||
impl ConstraintPair {
|
||||
pub fn new(lhs: TypeTerm, rhs: TypeTerm) -> Self {
|
||||
ConstraintPair {
|
||||
lhs,rhs, addr:vec![]
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub struct ConstraintSystem {
|
||||
σ: HashMap<TypeID, TypeTerm>,
|
||||
upper_bounds: HashMap< u64, TypeTerm >,
|
||||
lower_bounds: HashMap< u64, TypeTerm >,
|
||||
|
||||
equal_pairs: Vec<ConstraintPair>,
|
||||
subtype_pairs: Vec<ConstraintPair>,
|
||||
trait_pairs: Vec<ConstraintPair>,
|
||||
parallel_pairs: Vec<ConstraintPair>
|
||||
}
|
||||
|
||||
impl ConstraintSystem {
|
||||
pub fn new(
|
||||
equal_pairs: Vec<ConstraintPair>,
|
||||
subtype_pairs: Vec<ConstraintPair>,
|
||||
trait_pairs: Vec<ConstraintPair>,
|
||||
parallel_pairs: Vec<ConstraintPair>
|
||||
) -> Self {
|
||||
ConstraintSystem {
|
||||
σ: HashMap::new(),
|
||||
|
||||
equal_pairs,
|
||||
subtype_pairs,
|
||||
trait_pairs,
|
||||
parallel_pairs,
|
||||
|
||||
upper_bounds: HashMap::new(),
|
||||
lower_bounds: HashMap::new(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn new_eq(eqs: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new( eqs, Vec::new(), Vec::new(), Vec::new() )
|
||||
}
|
||||
|
||||
pub fn new_sub( subs: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new( Vec::new(), subs, Vec::new(), Vec::new() )
|
||||
}
|
||||
|
||||
pub fn new_trait(traits: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new( Vec::new(), Vec::new(), traits, Vec::new() )
|
||||
}
|
||||
|
||||
pub fn new_parallel( parallels: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new(Vec::new(), Vec::new(), Vec::new(), parallels )
|
||||
}
|
||||
|
||||
|
||||
/// update all values in substitution
|
||||
pub fn reapply_subst(&mut self) {
|
||||
let mut new_σ = HashMap::new();
|
||||
for (v, tt) in self.σ.iter() {
|
||||
let mut tt = tt.clone();
|
||||
tt.apply_subst(&self.σ);
|
||||
//eprintln!("update σ : {:?} --> {:?}", v, tt);
|
||||
new_σ.insert(v.clone(), tt.normalize());
|
||||
}
|
||||
self.σ = new_σ;
|
||||
}
|
||||
|
||||
|
||||
pub fn eval_equation(&mut self, unification_pair: ConstraintPair) -> Result<(), ConstraintError> {
|
||||
match (&unification_pair.lhs, &unification_pair.rhs) {
|
||||
(TypeTerm::TypeID(TypeID::Var(varid)), t) |
|
||||
(t, TypeTerm::TypeID(TypeID::Var(varid))) => {
|
||||
if ! t.contains_var( *varid ) {
|
||||
self.σ.insert(TypeID::Var(*varid), t.clone());
|
||||
self.reapply_subst();
|
||||
Ok(())
|
||||
} else if t == &TypeTerm::TypeID(TypeID::Var(*varid)) {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: TypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
|
||||
}
|
||||
}
|
||||
|
||||
(TypeTerm::TypeID(a1), TypeTerm::TypeID(a2)) => {
|
||||
if a1 == a2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
|
||||
}
|
||||
(TypeTerm::Num(n1), TypeTerm::Num(n2)) => {
|
||||
if n1 == n2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
|
||||
}
|
||||
(TypeTerm::Char(c1), TypeTerm::Char(c2)) => {
|
||||
if c1 == c2 { Ok(()) } else { Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
|
||||
}
|
||||
|
||||
(TypeTerm::Ladder(a1), TypeTerm::Ladder(a2)) |
|
||||
(TypeTerm::Spec(a1), TypeTerm::Spec(a2)) => {
|
||||
if a1.len() == a2.len() {
|
||||
for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push(
|
||||
ConstraintPair {
|
||||
lhs: x,
|
||||
rhs: y,
|
||||
addr: new_addr
|
||||
});
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
(TypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
|
||||
TypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
|
||||
=> {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(0);
|
||||
|
||||
if let Some(rhs_seq_repr) = rhs_seq_repr.as_ref() {
|
||||
if let Some(lhs_seq_repr) = lhs_seq_repr.as_ref() {
|
||||
let _seq_repr_ψ = self.eval_equation(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_seq_repr.clone(), rhs: *rhs_seq_repr.clone() })?;
|
||||
} else {
|
||||
return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if lhs_items.len() == rhs_items.len() {
|
||||
for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
|
||||
{
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
(TypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
|
||||
TypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
|
||||
=> {
|
||||
let new_addr = unification_pair.addr.clone();
|
||||
if let Some(rhs_struct_repr) = rhs_struct_repr.as_ref() {
|
||||
if let Some(lhs_struct_repr) = lhs_struct_repr.as_ref() {
|
||||
let _struct_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_struct_repr.clone(), rhs: *rhs_struct_repr.clone() })?;
|
||||
} else {
|
||||
return Err(ConstraintError{ addr: new_addr.clone(), t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
if lhs_members.len() == rhs_members.len() {
|
||||
for (i,
|
||||
(StructMember{ symbol: lhs_symbol, ty: lhs_ty},
|
||||
StructMember{ symbol: rhs_symbol, ty: rhs_ty })
|
||||
) in
|
||||
lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
|
||||
{
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
(TypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
|
||||
TypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
|
||||
=> {
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
if let Some(rhs_enum_repr) = rhs_enum_repr.as_ref() {
|
||||
if let Some(lhs_enum_repr) = lhs_enum_repr.as_ref() {
|
||||
let _enum_repr_ψ = self.eval_subtype(ConstraintPair { addr: new_addr.clone(), lhs: *lhs_enum_repr.clone(), rhs: *rhs_enum_repr.clone() })?;
|
||||
} else {
|
||||
return Err(ConstraintError{ addr: new_addr, t1: unification_pair.lhs, t2: unification_pair.rhs });
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
if lhs_variants.len() == rhs_variants.len() {
|
||||
for (i,
|
||||
(EnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
|
||||
EnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
|
||||
) in
|
||||
lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
|
||||
{
|
||||
let mut new_addr = unification_pair.addr.clone();
|
||||
new_addr.push(i);
|
||||
self.equal_pairs.push( ConstraintPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
|
||||
}
|
||||
Ok(())
|
||||
} else {
|
||||
Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
_ => Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> {
|
||||
|
||||
if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
if new_lower_bound.contains_var(v) {
|
||||
// loop
|
||||
return Err(());
|
||||
}
|
||||
|
||||
if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() {
|
||||
if let Ok(halo) = self.eval_subtype(
|
||||
ConstraintPair {
|
||||
lhs: lower_bound.clone(),
|
||||
rhs: new_lower_bound.clone(),
|
||||
addr: vec![]
|
||||
}
|
||||
) {
|
||||
// generalize variable type to supertype
|
||||
self.lower_bounds.insert(v, new_lower_bound);
|
||||
Ok(())
|
||||
} else if let Ok(halo) = self.eval_subtype(
|
||||
ConstraintPair{
|
||||
lhs: new_lower_bound,
|
||||
rhs: lower_bound,
|
||||
addr: vec![]
|
||||
}
|
||||
) {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(())
|
||||
}
|
||||
} else {
|
||||
self.lower_bounds.insert(v, new_lower_bound);
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: TypeTerm) -> Result<(),()> {
|
||||
if new_upper_bound == TypeTerm::TypeID(TypeID::Var(v)) {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
if new_upper_bound.contains_var(v) {
|
||||
// loop
|
||||
return Err(());
|
||||
}
|
||||
|
||||
if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() {
|
||||
if let Ok(_halo) = self.eval_subtype(
|
||||
ConstraintPair {
|
||||
lhs: new_upper_bound.clone(),
|
||||
rhs: upper_bound,
|
||||
addr: vec![]
|
||||
}
|
||||
) {
|
||||
eprintln!("found a lower upper bound: {} <= {:?}", v, new_upper_bound);
|
||||
// found a lower upper bound
|
||||
self.upper_bounds.insert(v, new_upper_bound);
|
||||
Ok(())
|
||||
} else {
|
||||
eprintln!("new upper bound violates subtype restriction");
|
||||
Err(())
|
||||
}
|
||||
} else {
|
||||
eprintln!("set upper bound: {} <= {:?}", v, new_upper_bound);
|
||||
self.upper_bounds.insert(v, new_upper_bound);
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
pub fn eval_subtype(&mut self, unification_pair: ConstraintPair) -> Result<
|
||||
// ok: halo type
|
||||
TypeTerm,
|
||||
|
|
@ -315,6 +27,7 @@ impl ConstraintSystem {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
(t, TypeTerm::TypeID(TypeID::Var(v))) => {
|
||||
//eprintln!("t <= variable");
|
||||
if self.add_lower_subtype_bound(v, t.clone()).is_ok() {
|
||||
|
|
@ -324,7 +37,6 @@ impl ConstraintSystem {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
Atoms
|
||||
*/
|
||||
|
|
@ -593,7 +305,7 @@ impl ConstraintSystem {
|
|||
reprψinterface
|
||||
]);
|
||||
}
|
||||
|
||||
|
||||
Ok(
|
||||
TypeTerm::Seq {
|
||||
seq_repr: if reprψ.is_empty() { None }
|
||||
|
|
@ -718,75 +430,4 @@ impl ConstraintSystem {
|
|||
_ => Err(ConstraintError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
|
||||
}
|
||||
}
|
||||
|
||||
pub fn solve(mut self) -> Result<(Vec<TypeTerm>, HashMap<TypeID, TypeTerm>), ConstraintError> {
|
||||
// solve equations
|
||||
while let Some( mut equal_pair ) = self.equal_pairs.pop() {
|
||||
equal_pair.lhs.apply_subst(&self.σ);
|
||||
equal_pair.rhs.apply_subst(&self.σ);
|
||||
|
||||
self.eval_equation(equal_pair)?;
|
||||
}
|
||||
|
||||
// solve subtypes
|
||||
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
|
||||
subtype_pair.lhs.apply_subst(&self.σ);
|
||||
subtype_pair.rhs.apply_subst(&self.σ);
|
||||
let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
|
||||
}
|
||||
|
||||
// add variables from subtype bounds
|
||||
for (var_id, t) in self.upper_bounds.iter() {
|
||||
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
|
||||
}
|
||||
|
||||
for (var_id, t) in self.lower_bounds.iter() {
|
||||
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
|
||||
}
|
||||
|
||||
self.reapply_subst();
|
||||
|
||||
|
||||
let mut halo_types = Vec::new();
|
||||
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
|
||||
subtype_pair.lhs = subtype_pair.lhs.apply_subst(&self.σ).clone();
|
||||
subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone();
|
||||
|
||||
let halo = self.eval_subtype( subtype_pair.clone() )?.strip();
|
||||
halo_types.push(halo);
|
||||
}
|
||||
|
||||
// solve traits
|
||||
while let Some( trait_pair ) = self.trait_pairs.pop() {
|
||||
unimplemented!();
|
||||
}
|
||||
|
||||
Ok((halo_types, self.σ))
|
||||
}
|
||||
}
|
||||
|
||||
pub fn unify(
|
||||
t1: &TypeTerm,
|
||||
t2: &TypeTerm
|
||||
) -> Result<HashMap<TypeID, TypeTerm>, ConstraintError> {
|
||||
let unification = ConstraintSystem::new_eq(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
|
||||
Ok(unification.solve()?.1)
|
||||
}
|
||||
|
||||
pub fn subtype_unify(
|
||||
t1: &TypeTerm,
|
||||
t2: &TypeTerm
|
||||
) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), ConstraintError> {
|
||||
let unification = ConstraintSystem::new_sub(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
|
||||
unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
|
||||
}
|
||||
|
||||
pub fn parallel_unify(
|
||||
t1: &TypeTerm,
|
||||
t2: &TypeTerm
|
||||
) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), ConstraintError> {
|
||||
let unification = ConstraintSystem::new_parallel(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
|
||||
unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
0
src/constraint_system/eval_trait.rs
Normal file
0
src/constraint_system/eval_trait.rs
Normal file
247
src/constraint_system/mod.rs
Normal file
247
src/constraint_system/mod.rs
Normal file
|
|
@ -0,0 +1,247 @@
|
|||
use {
|
||||
crate::{dict::*, term::TypeTerm, desugared_term::*, EnumVariant, StructMember, Substitution}, std::collections::HashMap
|
||||
};
|
||||
|
||||
pub mod eval_eq;
|
||||
pub mod eval_sub;
|
||||
pub mod eval_trait;
|
||||
pub mod eval_parallel;
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
||||
#[derive(Clone, Eq, PartialEq, Debug)]
|
||||
pub struct ConstraintError {
|
||||
pub addr: Vec<usize>,
|
||||
pub t1: TypeTerm,
|
||||
pub t2: TypeTerm
|
||||
}
|
||||
|
||||
#[derive(Clone, Eq, PartialEq, Debug)]
|
||||
pub struct ConstraintPair {
|
||||
pub addr: Vec<usize>,
|
||||
pub lhs: TypeTerm,
|
||||
pub rhs: TypeTerm,
|
||||
}
|
||||
|
||||
impl ConstraintPair {
|
||||
pub fn new(lhs: TypeTerm, rhs: TypeTerm) -> Self {
|
||||
ConstraintPair {
|
||||
lhs,rhs, addr:vec![]
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub struct ConstraintSystem {
|
||||
σ: HashMap<TypeID, TypeTerm>,
|
||||
upper_bounds: HashMap< u64, TypeTerm >,
|
||||
lower_bounds: HashMap< u64, TypeTerm >,
|
||||
|
||||
equal_pairs: Vec<ConstraintPair>,
|
||||
subtype_pairs: Vec<ConstraintPair>,
|
||||
trait_pairs: Vec<ConstraintPair>,
|
||||
parallel_pairs: Vec<ConstraintPair>
|
||||
}
|
||||
|
||||
impl ConstraintSystem {
|
||||
pub fn new(
|
||||
equal_pairs: Vec<ConstraintPair>,
|
||||
subtype_pairs: Vec<ConstraintPair>,
|
||||
trait_pairs: Vec<ConstraintPair>,
|
||||
parallel_pairs: Vec<ConstraintPair>
|
||||
) -> Self {
|
||||
ConstraintSystem {
|
||||
σ: HashMap::new(),
|
||||
|
||||
equal_pairs,
|
||||
subtype_pairs,
|
||||
trait_pairs,
|
||||
parallel_pairs,
|
||||
|
||||
upper_bounds: HashMap::new(),
|
||||
lower_bounds: HashMap::new(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn new_eq(eqs: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new( eqs, Vec::new(), Vec::new(), Vec::new() )
|
||||
}
|
||||
|
||||
pub fn new_sub( subs: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new( Vec::new(), subs, Vec::new(), Vec::new() )
|
||||
}
|
||||
|
||||
pub fn new_trait(traits: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new( Vec::new(), Vec::new(), traits, Vec::new() )
|
||||
}
|
||||
|
||||
pub fn new_parallel( parallels: Vec<ConstraintPair>) -> Self {
|
||||
ConstraintSystem::new(Vec::new(), Vec::new(), Vec::new(), parallels )
|
||||
}
|
||||
|
||||
|
||||
/// update all values in substitution
|
||||
pub fn reapply_subst(&mut self) {
|
||||
let mut new_σ = HashMap::new();
|
||||
for (v, tt) in self.σ.iter() {
|
||||
let mut tt = tt.clone();
|
||||
tt.apply_subst(&self.σ);
|
||||
//eprintln!("update σ : {:?} --> {:?}", v, tt);
|
||||
new_σ.insert(v.clone(), tt.normalize());
|
||||
}
|
||||
self.σ = new_σ;
|
||||
}
|
||||
|
||||
|
||||
pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: TypeTerm) -> Result<(),()> {
|
||||
|
||||
if new_lower_bound == TypeTerm::TypeID(TypeID::Var(v)) {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
if new_lower_bound.contains_var(v) {
|
||||
// loop
|
||||
return Err(());
|
||||
}
|
||||
|
||||
if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() {
|
||||
//eprintln!("var already exists. check max. type");
|
||||
if let Ok(halo) = self.eval_subtype(
|
||||
ConstraintPair {
|
||||
lhs: lower_bound.clone(),
|
||||
rhs: new_lower_bound.clone(),
|
||||
addr: vec![]
|
||||
}
|
||||
) {
|
||||
//eprintln!("found more general lower bound");
|
||||
//eprintln!("set var {}'s lowerbound to {:?}", v, new_lower_bound.clone());
|
||||
// generalize variable type to supertype
|
||||
self.lower_bounds.insert(v, new_lower_bound);
|
||||
Ok(())
|
||||
} else if let Ok(halo) = self.eval_subtype(
|
||||
ConstraintPair{
|
||||
lhs: new_lower_bound,
|
||||
rhs: lower_bound,
|
||||
addr: vec![]
|
||||
}
|
||||
) {
|
||||
//eprintln!("OK, is already larger type");
|
||||
Ok(())
|
||||
} else {
|
||||
//eprintln!("violated subtype restriction");
|
||||
Err(())
|
||||
}
|
||||
} else {
|
||||
//eprintln!("set var {}'s lowerbound to {:?}", v, new_lower_bound.clone());
|
||||
self.lower_bounds.insert(v, new_lower_bound);
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: TypeTerm) -> Result<(),()> {
|
||||
if new_upper_bound == TypeTerm::TypeID(TypeID::Var(v)) {
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
if new_upper_bound.contains_var(v) {
|
||||
// loop
|
||||
return Err(());
|
||||
}
|
||||
|
||||
if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() {
|
||||
if let Ok(_halo) = self.eval_subtype(
|
||||
ConstraintPair {
|
||||
lhs: new_upper_bound.clone(),
|
||||
rhs: upper_bound,
|
||||
addr: vec![]
|
||||
}
|
||||
) {
|
||||
//println!("found a lower upper bound: {} <= {:?}", v, new_upper_bound);
|
||||
// found a lower upper bound
|
||||
self.upper_bounds.insert(v, new_upper_bound);
|
||||
Ok(())
|
||||
} else {
|
||||
//println!("new upper bound violates subtype restriction");
|
||||
Err(())
|
||||
}
|
||||
} else {
|
||||
//eprintln!("set upper bound: {} <= {:?}", v, new_upper_bound);
|
||||
self.upper_bounds.insert(v, new_upper_bound);
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
pub fn solve(mut self) -> Result<(Vec<TypeTerm>, HashMap<TypeID, TypeTerm>), ConstraintError> {
|
||||
// solve equations
|
||||
while let Some( mut equal_pair ) = self.equal_pairs.pop() {
|
||||
equal_pair.lhs.apply_subst(&self.σ);
|
||||
equal_pair.rhs.apply_subst(&self.σ);
|
||||
|
||||
self.eval_equation(equal_pair)?;
|
||||
}
|
||||
|
||||
// solve subtypes
|
||||
//eprintln!("------ SOLVE SUBTYPES ---- ");
|
||||
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
|
||||
subtype_pair.lhs.apply_subst(&self.σ);
|
||||
subtype_pair.rhs.apply_subst(&self.σ);
|
||||
let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
|
||||
}
|
||||
|
||||
// add variables from subtype bounds
|
||||
for (var_id, t) in self.upper_bounds.iter() {
|
||||
// eprintln!("VAR {} upper bound {:?}", var_id, t);
|
||||
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
|
||||
}
|
||||
|
||||
for (var_id, t) in self.lower_bounds.iter() {
|
||||
// eprintln!("VAR {} lower bound {:?}", var_id, t);
|
||||
self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
|
||||
}
|
||||
|
||||
self.reapply_subst();
|
||||
|
||||
//eprintln!("------ MAKE HALOS -----");
|
||||
let mut halo_types = Vec::new();
|
||||
for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
|
||||
subtype_pair.lhs = subtype_pair.lhs.apply_subst(&self.σ).clone();
|
||||
subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone();
|
||||
|
||||
let halo = self.eval_subtype( subtype_pair.clone() )?.strip();
|
||||
halo_types.push(halo);
|
||||
}
|
||||
|
||||
// solve traits
|
||||
while let Some( trait_pair ) = self.trait_pairs.pop() {
|
||||
unimplemented!();
|
||||
}
|
||||
|
||||
Ok((halo_types, self.σ))
|
||||
}
|
||||
}
|
||||
|
||||
pub fn unify(
|
||||
t1: &TypeTerm,
|
||||
t2: &TypeTerm
|
||||
) -> Result<HashMap<TypeID, TypeTerm>, ConstraintError> {
|
||||
let unification = ConstraintSystem::new_eq(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
|
||||
Ok(unification.solve()?.1)
|
||||
}
|
||||
|
||||
pub fn subtype_unify(
|
||||
t1: &TypeTerm,
|
||||
t2: &TypeTerm
|
||||
) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), ConstraintError> {
|
||||
let unification = ConstraintSystem::new_sub(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
|
||||
unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
|
||||
}
|
||||
|
||||
pub fn parallel_unify(
|
||||
t1: &TypeTerm,
|
||||
t2: &TypeTerm
|
||||
) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), ConstraintError> {
|
||||
let unification = ConstraintSystem::new_parallel(vec![ ConstraintPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
|
||||
unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
|
||||
}
|
||||
|
||||
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
|
||||
use {
|
||||
crate::{dict::*, parser::*, constraint_system::ConstraintError},
|
||||
crate::{dict::*, parser::*, constraint_system::{ConstraintError}},
|
||||
std::iter::FromIterator
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue