forked from M-Labs/nac3
more tests
This commit is contained in:
parent
929b7e1d92
commit
87dd0ee3cb
@ -16,15 +16,24 @@ fn find_subst(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
let mut substituted = false;
|
||||||
if let TypeVariable(id) = b.as_ref() {
|
if let TypeVariable(id) = b.as_ref() {
|
||||||
if let Some(c) = sub.get(&id) {
|
if let Some(c) = sub.get(&id) {
|
||||||
b = c.clone();
|
b = c.clone();
|
||||||
|
substituted = true;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
match (a.as_ref(), b.as_ref()) {
|
match (a.as_ref(), b.as_ref()) {
|
||||||
(BotType, _) => Ok(()),
|
(BotType, _) => Ok(()),
|
||||||
(TypeVariable(id_a), TypeVariable(id_b)) => {
|
(TypeVariable(id_a), TypeVariable(id_b)) => {
|
||||||
|
if substituted {
|
||||||
|
return if id_a == id_b {
|
||||||
|
Ok(())
|
||||||
|
} else {
|
||||||
|
Err("different variables".to_string())
|
||||||
|
};
|
||||||
|
}
|
||||||
let v_a = ctx.get_variable(*id_a);
|
let v_a = ctx.get_variable(*id_a);
|
||||||
let v_b = ctx.get_variable(*id_b);
|
let v_b = ctx.get_variable(*id_b);
|
||||||
if v_b.bound.len() > 0 {
|
if v_b.bound.len() > 0 {
|
||||||
@ -224,6 +233,17 @@ mod tests {
|
|||||||
Err("different domain".to_string())
|
Err("different domain".to_string())
|
||||||
);
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
None,
|
||||||
|
"float",
|
||||||
|
create_tuple(vec![]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Err("different parametric types".to_string())
|
||||||
|
);
|
||||||
|
|
||||||
let v1 = ctx.add_variable(VarDef {
|
let v1 = ctx.add_variable(VarDef {
|
||||||
name: "V1",
|
name: "V1",
|
||||||
bound: vec![
|
bound: vec![
|
||||||
@ -269,6 +289,10 @@ mod tests {
|
|||||||
let mut ctx = basic_ctx();
|
let mut ctx = basic_ctx();
|
||||||
let mut assumptions = HashMap::new();
|
let mut assumptions = HashMap::new();
|
||||||
|
|
||||||
|
let v0 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
||||||
|
name: "V0",
|
||||||
|
bound: vec![],
|
||||||
|
})));
|
||||||
let v1 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
let v1 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
||||||
name: "V1",
|
name: "V1",
|
||||||
bound: vec![
|
bound: vec![
|
||||||
@ -340,6 +364,26 @@ mod tests {
|
|||||||
),
|
),
|
||||||
Ok(Some(v1.clone()))
|
Ok(Some(v1.clone()))
|
||||||
);
|
);
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
Some(v0.clone()),
|
||||||
|
"__add__",
|
||||||
|
create_tuple(vec![v2.clone()]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Err("unbounded type var".to_string())
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
Some(v1.clone()),
|
||||||
|
"__add__",
|
||||||
|
create_tuple(vec![v0.clone()]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Err("different domain".to_string())
|
||||||
|
);
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
resolve_call(
|
resolve_call(
|
||||||
&ctx,
|
&ctx,
|
||||||
@ -350,6 +394,16 @@ mod tests {
|
|||||||
),
|
),
|
||||||
Err("different domain".to_string())
|
Err("different domain".to_string())
|
||||||
);
|
);
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
Some(v1.clone()),
|
||||||
|
"__add__",
|
||||||
|
create_tuple(vec![v3.clone()]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Err("different domain".to_string())
|
||||||
|
);
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
resolve_call(
|
resolve_call(
|
||||||
&ctx,
|
&ctx,
|
||||||
@ -370,7 +424,66 @@ mod tests {
|
|||||||
),
|
),
|
||||||
Err("no such function".to_string())
|
Err("no such function".to_string())
|
||||||
);
|
);
|
||||||
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn test_multi_generic() {
|
||||||
|
let mut ctx = basic_ctx();
|
||||||
|
let mut assumptions = HashMap::new();
|
||||||
|
let v0 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
||||||
|
name: "V0",
|
||||||
|
bound: vec![],
|
||||||
|
})));
|
||||||
|
let v1 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
||||||
|
name: "V1",
|
||||||
|
bound: vec![],
|
||||||
|
})));
|
||||||
|
let v2 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
||||||
|
name: "V2",
|
||||||
|
bound: vec![],
|
||||||
|
})));
|
||||||
|
let v3 = Rc::new(TypeVariable(ctx.add_variable(VarDef {
|
||||||
|
name: "V3",
|
||||||
|
bound: vec![],
|
||||||
|
})));
|
||||||
|
|
||||||
|
ctx.add_fn(
|
||||||
|
"foo",
|
||||||
|
FnDef {
|
||||||
|
args: create_tuple(vec![v0.clone(), v0.clone(), v1.clone()]),
|
||||||
|
result: Some(v0.clone()),
|
||||||
|
},
|
||||||
|
);
|
||||||
|
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
None,
|
||||||
|
"foo",
|
||||||
|
create_tuple(vec![v2.clone(), v2.clone(), v2.clone()]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Ok(Some(v2.clone()))
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
None,
|
||||||
|
"foo",
|
||||||
|
create_tuple(vec![v2.clone(), v2.clone(), v3.clone()]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Ok(Some(v2.clone()))
|
||||||
|
);
|
||||||
|
assert_eq!(
|
||||||
|
resolve_call(
|
||||||
|
&ctx,
|
||||||
|
None,
|
||||||
|
"foo",
|
||||||
|
create_tuple(vec![v2.clone(), v3.clone(), v3.clone()]),
|
||||||
|
&mut assumptions
|
||||||
|
),
|
||||||
|
Err("different variables".to_string())
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user