forked from M-Labs/nac3
refactored using constrain
to allow easier modification later with subtyping
This commit is contained in:
parent
e732f7e089
commit
eb4b2bb7f6
@ -38,6 +38,12 @@ impl<'a> Fold<()> for Inferencer<'a> {
|
|||||||
type InferenceResult = Result<Type, String>;
|
type InferenceResult = Result<Type, String>;
|
||||||
|
|
||||||
impl<'a> Inferencer<'a> {
|
impl<'a> Inferencer<'a> {
|
||||||
|
/// Constrain a <: b
|
||||||
|
/// Currently implemented as unification
|
||||||
|
fn constrain(&mut self, a: Type, b: Type) -> Result<(), String> {
|
||||||
|
self.unifier.unify(a, b)
|
||||||
|
}
|
||||||
|
|
||||||
fn build_method_call(
|
fn build_method_call(
|
||||||
&mut self,
|
&mut self,
|
||||||
method: String,
|
method: String,
|
||||||
@ -55,7 +61,7 @@ impl<'a> Inferencer<'a> {
|
|||||||
let call = self.unifier.add_ty(TypeEnum::TCall { calls: vec![call] });
|
let call = self.unifier.add_ty(TypeEnum::TCall { calls: vec![call] });
|
||||||
let fields = once((method, call)).collect();
|
let fields = once((method, call)).collect();
|
||||||
let record = self.unifier.add_ty(TypeEnum::TRecord { fields });
|
let record = self.unifier.add_ty(TypeEnum::TRecord { fields });
|
||||||
self.unifier.unify(obj, record)?;
|
self.constrain(obj, record)?;
|
||||||
Ok(ret)
|
Ok(ret)
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -114,15 +120,15 @@ impl<'a> Inferencer<'a> {
|
|||||||
fn infer_attribute(&mut self, value: &ast::Expr<Option<Type>>, attr: &str) -> InferenceResult {
|
fn infer_attribute(&mut self, value: &ast::Expr<Option<Type>>, attr: &str) -> InferenceResult {
|
||||||
let (attr_ty, _) = self.unifier.get_fresh_var();
|
let (attr_ty, _) = self.unifier.get_fresh_var();
|
||||||
let fields = once((attr.to_string(), attr_ty)).collect();
|
let fields = once((attr.to_string(), attr_ty)).collect();
|
||||||
let parent = self.unifier.add_ty(TypeEnum::TRecord { fields });
|
let record = self.unifier.add_ty(TypeEnum::TRecord { fields });
|
||||||
self.unifier.unify(value.custom.unwrap(), parent)?;
|
self.constrain(value.custom.unwrap(), record)?;
|
||||||
Ok(attr_ty)
|
Ok(attr_ty)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn infer_bool_ops(&mut self, values: &[ast::Expr<Option<Type>>]) -> InferenceResult {
|
fn infer_bool_ops(&mut self, values: &[ast::Expr<Option<Type>>]) -> InferenceResult {
|
||||||
let b = self.primitives.bool;
|
let b = self.primitives.bool;
|
||||||
for v in values {
|
for v in values {
|
||||||
self.unifier.unify(v.custom.unwrap(), b)?;
|
self.constrain(v.custom.unwrap(), b)?;
|
||||||
}
|
}
|
||||||
Ok(b)
|
Ok(b)
|
||||||
}
|
}
|
||||||
@ -181,32 +187,30 @@ impl<'a> Inferencer<'a> {
|
|||||||
.iter()
|
.iter()
|
||||||
.flatten()
|
.flatten()
|
||||||
{
|
{
|
||||||
self.unifier
|
self.constrain(v.custom.unwrap(), self.primitives.int32)?;
|
||||||
.unify(self.primitives.int32, v.custom.unwrap())?;
|
|
||||||
}
|
}
|
||||||
let list = self.unifier.add_ty(TypeEnum::TList { ty });
|
let list = self.unifier.add_ty(TypeEnum::TList { ty });
|
||||||
self.unifier.unify(value.custom.unwrap(), list)?;
|
self.constrain(value.custom.unwrap(), list)?;
|
||||||
Ok(list)
|
Ok(list)
|
||||||
}
|
}
|
||||||
ast::ExprKind::Constant {
|
ast::ExprKind::Constant {
|
||||||
value: ast::Constant::Int(val),
|
value: ast::Constant::Int(val),
|
||||||
..
|
..
|
||||||
} => {
|
} => {
|
||||||
// the index is a constant, so value can be a sequence (either list/tuple)
|
// the index is a constant, so value can be a sequence.
|
||||||
let ind: i32 = val
|
let ind: i32 = val
|
||||||
.try_into()
|
.try_into()
|
||||||
.map_err(|_| "Index must be int32".to_string())?;
|
.map_err(|_| "Index must be int32".to_string())?;
|
||||||
let map = once((ind, ty)).collect();
|
let map = once((ind, ty)).collect();
|
||||||
let seq = self.unifier.add_ty(TypeEnum::TSeq { map });
|
let seq = self.unifier.add_ty(TypeEnum::TSeq { map });
|
||||||
self.unifier.unify(value.custom.unwrap(), seq)?;
|
self.constrain(value.custom.unwrap(), seq)?;
|
||||||
Ok(ty)
|
Ok(ty)
|
||||||
}
|
}
|
||||||
_ => {
|
_ => {
|
||||||
// the index is not a constant, so value can only be a list
|
// the index is not a constant, so value can only be a list
|
||||||
self.unifier
|
self.constrain(slice.custom.unwrap(), self.primitives.int32)?;
|
||||||
.unify(slice.custom.unwrap(), self.primitives.int32)?;
|
|
||||||
let list = self.unifier.add_ty(TypeEnum::TList { ty });
|
let list = self.unifier.add_ty(TypeEnum::TList { ty });
|
||||||
self.unifier.unify(value.custom.unwrap(), list)?;
|
self.constrain(value.custom.unwrap(), list)?;
|
||||||
Ok(ty)
|
Ok(ty)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -218,10 +222,10 @@ impl<'a> Inferencer<'a> {
|
|||||||
body: ast::Expr<Option<Type>>,
|
body: ast::Expr<Option<Type>>,
|
||||||
orelse: ast::Expr<Option<Type>>,
|
orelse: ast::Expr<Option<Type>>,
|
||||||
) -> InferenceResult {
|
) -> InferenceResult {
|
||||||
self.unifier
|
self.constrain(test.custom.unwrap(), self.primitives.bool)?;
|
||||||
.unify(test.custom.unwrap(), self.primitives.bool)?;
|
let ty = self.unifier.get_fresh_var().0;
|
||||||
self.unifier
|
self.constrain(body.custom.unwrap(), ty)?;
|
||||||
.unify(body.custom.unwrap(), orelse.custom.unwrap())?;
|
self.constrain(orelse.custom.unwrap(), ty)?;
|
||||||
Ok(body.custom.unwrap())
|
Ok(ty)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -188,9 +188,7 @@ impl Unifier {
|
|||||||
)
|
)
|
||||||
};
|
};
|
||||||
|
|
||||||
let (ty_a, ty_b) = {
|
let (ty_a, ty_b) = { (ty_a_cell.borrow(), ty_b_cell.borrow()) };
|
||||||
(ty_a_cell.borrow(), ty_b_cell.borrow())
|
|
||||||
};
|
|
||||||
|
|
||||||
self.occur_check(a, b)?;
|
self.occur_check(a, b)?;
|
||||||
match (&*ty_a, &*ty_b) {
|
match (&*ty_a, &*ty_b) {
|
||||||
|
Loading…
Reference in New Issue
Block a user