forked from M-Labs/nac3
1
0
Fork 0

removed method for type variables

This commit is contained in:
pca006132 2021-06-25 16:08:32 +08:00
parent ed28c09c51
commit 5292f32835
3 changed files with 7 additions and 107 deletions

View File

@ -185,22 +185,6 @@ impl TypeEnum {
} }
} }
pub fn inv_subst(&self, map: &[(Type, Type)]) -> Type {
for (from, to) in map.iter() {
if self == from.as_ref() {
return to.clone();
}
}
match self {
TypeEnum::ParametricType(id, params) => TypeEnum::ParametricType(
*id,
params.iter().map(|v| v.as_ref().inv_subst(map)).collect(),
),
_ => self.clone(),
}
.into()
}
pub fn get_subst(&self, ctx: &InferenceContext) -> HashMap<VariableId, Type> { pub fn get_subst(&self, ctx: &InferenceContext) -> HashMap<VariableId, Type> {
match self { match self {
TypeEnum::ParametricType(id, params) => { TypeEnum::ParametricType(id, params) => {

View File

@ -658,7 +658,7 @@ mod test {
let ast = parse_expression("a + a + a").unwrap(); let ast = parse_expression("a + a + a").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
assert_eq!(result.unwrap().unwrap(), TypeVariable(v0).into()); assert_eq!(result, Err("not supported".into()));
} }
#[test] #[test]
@ -677,7 +677,7 @@ mod test {
let ast = parse_expression("-a").unwrap(); let ast = parse_expression("-a").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
assert_eq!(result.unwrap().unwrap(), TypeVariable(v0).into()); assert_eq!(result, Err("not supported".into()));
let ast = parse_expression("not True").unwrap(); let ast = parse_expression("not True").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
@ -700,11 +700,11 @@ mod test {
let ast = parse_expression("a == a == a").unwrap(); let ast = parse_expression("a == a == a").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
assert_eq!(result.unwrap().unwrap(), ctx.get_primitive(BOOL_TYPE)); assert_eq!(result, Err("not supported".into()));
let ast = parse_expression("a == a == 1").unwrap(); let ast = parse_expression("a == a == 1").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
assert_eq!(result, Err("not equal".into())); assert_eq!(result, Err("not supported".into()));
let ast = parse_expression("True > False").unwrap(); let ast = parse_expression("True > False").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
@ -792,7 +792,7 @@ mod test {
let ast = parse_expression("v1.a()").unwrap(); let ast = parse_expression("v1.a()").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
assert_eq!(result.unwrap().unwrap(), TypeVariable(v1).into()); assert_eq!(result, Err("not supported".into()));
let ast = parse_expression("foobar.a()").unwrap(); let ast = parse_expression("foobar.a()").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
@ -809,14 +809,6 @@ mod test {
let ast = parse_expression("[][0].a()").unwrap(); let ast = parse_expression("[][0].a()").unwrap();
let result = infer_expr(&mut ctx, &ast); let result = infer_expr(&mut ctx, &ast);
assert_eq!(result, Err("not supported".into())); assert_eq!(result, Err("not supported".into()));
let ast = parse_expression("v0.a()").unwrap();
let result = infer_expr(&mut ctx, &ast);
assert_eq!(result, Err("unbounded type var".into()));
let ast = parse_expression("v2.a()").unwrap();
let result = infer_expr(&mut ctx, &ast);
assert_eq!(result, Err("no such function".into()));
} }
#[test] #[test]

View File

@ -129,39 +129,6 @@ fn resolve_call_rec(
let fun = match &obj { let fun = match &obj {
Some(obj) => { Some(obj) => {
let base = match obj.as_ref() { let base = match obj.as_ref() {
TypeVariable(id) => {
let v = ctx.get_variable_def(*id);
if v.bound.is_empty() {
return Err("unbounded type var".to_string());
}
let results: Result<Vec<_>, String> = v
.bound
.iter()
.map(|ins| {
resolve_call_rec(
ctx,
&Some((*id, ins.clone())),
Some(ins.clone()),
func,
args.clone(),
)
})
.collect();
let results = results?;
if results.iter().all(|v| v == &results[0]) {
return Ok(results[0].clone());
}
let mut results = results.iter().zip(v.bound.iter()).map(|(r, ins)| {
r.as_ref()
.map(|v| v.inv_subst(&[(ins.clone(), obj.clone())]))
});
let first = results.next().unwrap();
if results.all(|v| v == first) {
return Ok(first);
} else {
return Err("divergent type after substitution".to_string());
}
}
PrimitiveType(id) => &ctx.get_primitive_def(*id), PrimitiveType(id) => &ctx.get_primitive_def(*id),
ClassType(id) | VirtualClassType(id) => &ctx.get_class_def(*id).base, ClassType(id) | VirtualClassType(id) => &ctx.get_class_def(*id).base,
ParametricType(id, _) => &ctx.get_parametric_def(*id).base, ParametricType(id, _) => &ctx.get_parametric_def(*id).base,
@ -273,25 +240,6 @@ mod tests {
bound: vec![], bound: vec![],
}); });
let v0 = ctx.get_variable(v0); let v0 = ctx.get_variable(v0);
let v1 = ctx.add_variable(VarDef {
name: "V1",
bound: vec![ctx.get_primitive(INT32_TYPE), ctx.get_primitive(FLOAT_TYPE)],
});
let v1 = ctx.get_variable(v1);
let v2 = ctx.add_variable(VarDef {
name: "V2",
bound: vec![ctx.get_primitive(INT32_TYPE), ctx.get_primitive(FLOAT_TYPE)],
});
let v2 = ctx.get_variable(v2);
let v3 = ctx.add_variable(VarDef {
name: "V3",
bound: vec![
ctx.get_primitive(BOOL_TYPE),
ctx.get_primitive(INT32_TYPE),
ctx.get_primitive(FLOAT_TYPE),
],
});
let v3 = ctx.get_variable(v3);
let int32 = ctx.get_primitive(INT32_TYPE); let int32 = ctx.get_primitive(INT32_TYPE);
let int64 = ctx.get_primitive(INT64_TYPE); let int64 = ctx.get_primitive(INT64_TYPE);
@ -315,32 +263,8 @@ mod tests {
// with type variables // with type variables
assert_eq!( assert_eq!(
resolve_call(&ctx, Some(v1.clone()), "__add__", &[v1.clone()]), resolve_call(&ctx, Some(v0.clone()), "__add__", &[v0.clone()]),
Ok(Some(v1.clone())) Err("not supported".into())
);
assert_eq!(
resolve_call(&ctx, Some(v0.clone()), "__add__", &[v2.clone()]),
Err("unbounded type var".to_string())
);
assert_eq!(
resolve_call(&ctx, Some(v1.clone()), "__add__", &[v0]),
Err("different domain".to_string())
);
assert_eq!(
resolve_call(&ctx, Some(v1.clone()), "__add__", &[v2]),
Err("different domain".to_string())
);
assert_eq!(
resolve_call(&ctx, Some(v1.clone()), "__add__", &[v3.clone()]),
Err("different domain".to_string())
);
assert_eq!(
resolve_call(&ctx, Some(v3.clone()), "__add__", &[v1]),
Err("no such function".to_string())
);
assert_eq!(
resolve_call(&ctx, Some(v3.clone()), "__add__", &[v3]),
Err("no such function".to_string())
); );
} }