ProvableHQ/leo
1
1
Fork 0
mirror of https://github.com/ProvableHQ/leo.git synced 2024-12-27 04:01:47 +03:00
Code Issues Packages Projects Releases Wiki Activity

enforce order on solving type assertions

Browse Source
This commit is contained in:
collin 2020-10-23 17:59:34 -07:00
parent f2a808cbe7
commit d55bd0d2af
1 changed files with 26 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
dynamic-check/src/dynamic_check.rs
View File

@ -1237,10 +1237,20 @@ impl Frame {
fn solve(self) -> Result<(), FrameError> {
let mut unsolved = self.type_assertions.clone();
// Solve all type equality assertions first.
let mut unsolved_membership = Vec::new();
while !unsolved.is_empty() {
// Pop type assertion from list
let type_assertion = unsolved.pop().unwrap();
// If it is a membership assertion, then skip it for now.
if let TypeAssertion::Membership(membership) = type_assertion {
unsolved_membership.push(membership);
continue;
}
println!("assertion: {:?}", type_assertion);
// Solve the `TypeAssertion`.
@ -1253,9 +1263,22 @@ impl Frame {
for original in &mut unsolved {
original.substitute(&pair.0, &pair.1)
}
for original in &mut unsolved_membership {
original.substitute(&pair.0, &pair.1)
}
};
}
// Solve all type membership assertions.
while !unsolved_membership.is_empty() {
// Pop type assertion from list
let type_assertion = unsolved_membership.pop().unwrap();
// Solve the membership assertion.
type_assertion.solve()?;
}
// for type_assertion in unsolved.pop() {
// if let Some((type_variable, type_)) = type_assertion.get_substitute() {
// // Substitute type variable in unsolved type assertions
@ -1427,7 +1450,7 @@ impl TypeAssertion {
pub fn substitute(&mut self, variable: &TypeVariable, type_: &Type) {
match self {
TypeAssertion::Equality(equality) => equality.substitute(variable, type_),
TypeAssertion::Membership(_) => unimplemented!(),
TypeAssertion::Membership(membership) => membership.substitute(variable, type_),
}
}
@ -1472,9 +1495,8 @@ impl TypeMembership {
///
/// Substitutes the given `TypeVariable` for each `Type` in the `TypeMembership`.
///
pub fn substitute(&mut self, _variable: &TypeVariable, _type_: &Type) {
// self.left.substitute(variable, type_);
// self.right.substitute(variable, type_);
pub fn substitute(&mut self, variable: &TypeVariable, type_: &Type) {
self.given.substitute(variable, type_)
}
///