Migrate ability resolution tests

This commit is contained in:
Ayaz Hafiz 2023-04-02 13:02:01 -05:00
parent 05af17af43
commit 88b044a765
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
12 changed files with 215 additions and 380 deletions

View file

@ -6120,386 +6120,6 @@ mod solve_expr {
)
}
#[test]
fn resolve_lambda_set_generalized_ability_alias() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1}
main =
alias1 = \x -> id x
# ^^
alias2 = \x -> alias1 x
# ^^^^^^
a : A
a = alias2 (@A {})
# ^^^^^^
a
"#
),
@r###"
A#id(4) : A -[[id(4)]]-> A
Id#id(2) : a -[[] + a:id(2):1]-> a | a has Id
alias1 : a -[[alias1(6)]]-> a | a has Id
alias2 : A -[[alias2(7)]]-> A
"###
)
}
#[test]
fn resolve_lambda_set_weakened_ability_alias() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1}
main =
# Both alias1, alias2 should get weakened
alias1 = id
# ^^
alias2 = alias1
# ^^^^^^
a : A
a = alias2 (@A {})
# ^^^^^^
a
"#
),
@r###"
A#id(4) : A -[[id(4)]]-> A
Id#id(2) : A -[[id(4)]]-> A
alias1 : A -[[id(4)]]-> A
alias2 : A -[[id(4)]]-> A
"###
)
}
#[test]
fn resolve_lambda_set_ability_chain() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Id1 has id1 : a -> a | a has Id1
Id2 has id2 : a -> a | a has Id2
A := {} has [Id1 {id1}, Id2 {id2}]
id1 = \@A {} -> @A {}
#^^^{-1}
id2 = \@A {} -> id1 (@A {})
#^^^{-1} ^^^
main =
a : A
a = id2 (@A {})
# ^^^
a
"#
),
@r###"
A#id1(6) : A -[[id1(6)]]-> A
A#id2(7) : A -[[id2(7)]]-> A
A#id1(6) : A -[[id1(6)]]-> A
A#id2(7) : A -[[id2(7)]]-> A
"###
)
}
#[test]
fn resolve_lambda_set_branches_ability_vs_non_ability() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1}
idNotAbility = \x -> x
#^^^^^^^^^^^^{-1}
main =
choice : [T, U]
# Should not get generalized
idChoice =
#^^^^^^^^{-1}
when choice is
T -> id
U -> idNotAbility
idChoice (@A {})
#^^^^^^^^{-1}
"#
),
@r###"
A#id(4) : A -[[id(4)]]-> A
idNotAbility : a -[[idNotAbility(5)]]-> a
idChoice : A -[[id(4), idNotAbility(5)]]-> A
idChoice : A -[[id(4), idNotAbility(5)]]-> A
"###
)
}
#[test]
fn resolve_lambda_set_branches_same_ability() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1}
main =
choice : [T, U]
# Should not get generalized
idChoice =
#^^^^^^^^{-1}
when choice is
T -> id
U -> id
idChoice (@A {})
#^^^^^^^^{-1}
"#
),
@r#"
A#id(4) : A -[[id(4)]]-> A
idChoice : A -[[id(4)]]-> A
idChoice : A -[[id(4)]]-> A
"#
)
}
#[test]
fn resolve_unspecialized_lambda_set_behind_alias() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Thunk a : {} -> a
Id has id : a -> Thunk a | a has Id
A := {} has [Id {id}]
id = \@A {} -> \{} -> @A {}
#^^{-1}
main =
alias = \x -> id x
# ^^
a : A
a = (alias (@A {})) {}
# ^^^^^
a
"#
),
@r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8]]-> {})
Id#id(3) : a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) | a has Id
alias : {} -[[alias(9)]]-> ({} -[[8]]-> {})
"#
print_only_under_alias: true
)
}
#[test]
fn resolve_unspecialized_lambda_set_behind_opaque() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Thunk a := {} -> a
Id has id : a -> Thunk a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @Thunk (\{} -> @A {})
#^^{-1}
main =
thunk = id (@A {})
@Thunk it = thunk
it {}
#^^{-1}
"#
),
@r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8]]-> {})
it : {} -[[8]]-> {}
"#
print_only_under_alias: true
)
}
#[test]
fn resolve_two_unspecialized_lambda_sets_in_one_lambda_set() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Thunk a : {} -> a
Id has id : a -> Thunk a | a has Id
A := {} has [Id {id}]
id = \@A {} -> \{} -> @A {}
#^^{-1}
main =
a : A
a = (id (@A {})) {}
# ^^
a
"#
),
@r#"
A#id(5) : {} -[[id(5)]]-> ({} -[[8]]-> {})
A#id(5) : {} -[[id(5)]]-> ({} -[[8]]-> {})
"#
print_only_under_alias: true
)
}
#[test]
fn resolve_recursive_ability_lambda_set() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Diverge has diverge : a -> a | a has Diverge
A := {} has [Diverge {diverge}]
diverge : A -> A
diverge = \@A {} -> diverge (@A {})
#^^^^^^^{-1} ^^^^^^^
main =
a : A
a = diverge (@A {})
# ^^^^^^^
a
"#
),
@r###"
A#diverge(4) : A -[[diverge(4)]]-> A
A#diverge(4) : A -[[diverge(4)]]-> A
A#diverge(4) : A -[[diverge(4)]]-> A
"###
)
}
#[test]
fn resolve_mutually_recursive_ability_lambda_sets() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Bounce has
ping : a -> a | a has Bounce
pong : a -> a | a has Bounce
A := {} has [Bounce {ping: pingA, pong: pongA}]
pingA = \@A {} -> pong (@A {})
#^^^^^{-1} ^^^^
pongA = \@A {} -> ping (@A {})
#^^^^^{-1} ^^^^
main =
a : A
a = ping (@A {})
# ^^^^
a
"#
),
@r###"
pingA : A -[[pingA(5)]]-> A
A#pong(6) : A -[[pongA(6)]]-> A
pongA : A -[[pongA(6)]]-> A
A#ping(5) : A -[[pingA(5)]]-> A
A#ping(5) : A -[[pingA(5)]]-> A
"###
)
}
#[test]
fn resolve_mutually_recursive_ability_lambda_sets_inferred() {
infer_queries!(
indoc!(
r#"
app "test" provides [main] to "./platform"
Bounce has
ping : a -> a | a has Bounce
pong : a -> a | a has Bounce
A := {} has [Bounce {ping, pong}]
ping = \@A {} -> pong (@A {})
#^^^^{-1} ^^^^
pong = \@A {} -> ping (@A {})
#^^^^{-1} ^^^^
main =
a : A
a = ping (@A {})
# ^^^^
a
"#
),
@r###"
A#ping(5) : A -[[ping(5)]]-> A
A#pong(6) : A -[[pong(6)]]-> A
A#pong(6) : A -[[pong(6)]]-> A
A#ping(5) : A -[[ping(5)]]-> A
A#ping(5) : A -[[ping(5)]]-> A
"###
)
}
#[test]
fn list_of_lambdas() {
infer_queries!(

View file

@ -0,0 +1,19 @@
app "test" provides [main] to "./platform"
Id1 has id1 : a -> a | a has Id1
Id2 has id2 : a -> a | a has Id2
A := {} has [Id1 {id1}, Id2 {id2}]
id1 = \@A {} -> @A {}
#^^^{-1} A#id1(6): A -[[id1(6)]]-> A
id2 = \@A {} -> id1 (@A {})
# ^^^ A#id1(6): A -[[id1(6)]]-> A
#^^^{-1} A#id2(7): A -[[id2(7)]]-> A
main =
a : A
a = id2 (@A {})
# ^^^ A#id2(7): A -[[id2(7)]]-> A
a

View file

@ -0,0 +1,23 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A
idNotAbility = \x -> x
#^^^^^^^^^^^^{-1} a -[[idNotAbility(5)]]-> a
main =
choice : [T, U]
# Should not get generalized
idChoice =
#^^^^^^^^{-1} A -[[id(4), idNotAbility(5)]]-> A
when choice is
T -> id
U -> idNotAbility
idChoice (@A {})
#^^^^^^^^{-1} A -[[id(4), idNotAbility(5)]]-> A

View file

@ -0,0 +1,20 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A
main =
choice : [T, U]
# Should not get generalized
idChoice =
#^^^^^^^^{-1} A -[[id(4)]]-> A
when choice is
T -> id
U -> id
idChoice (@A {})
#^^^^^^^^{-1} A -[[id(4)]]-> A

View file

@ -0,0 +1,19 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A
main =
alias1 = \x -> id x
# ^^ Id#id(2): a -[[] + a:id(2):1]-> a | a has Id
alias2 = \x -> alias1 x
# ^^^^^^ a -[[alias1(6)]]-> a | a has Id
a : A
a = alias2 (@A {})
# ^^^^^^ A -[[alias2(7)]]-> A
a

View file

@ -0,0 +1,20 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A
main =
# Both alias1, alias2 should get weakened
alias1 = id
# ^^ Id#id(2): A -[[id(4)]]-> A
alias2 = alias1
# ^^^^^^ A -[[id(4)]]-> A
a : A
a = alias2 (@A {})
# ^^^^^^ A -[[id(4)]]-> A
a

View file

@ -0,0 +1,22 @@
app "test" provides [main] to "./platform"
Bounce has
ping : a -> a | a has Bounce
pong : a -> a | a has Bounce
A := {} has [Bounce {ping: pingA, pong: pongA}]
pingA = \@A {} -> pong (@A {})
# ^^^^ A#pong(6): A -[[pongA(6)]]-> A
#^^^^^{-1} A -[[pingA(5)]]-> A
pongA = \@A {} -> ping (@A {})
# ^^^^ A#ping(5): A -[[pingA(5)]]-> A
#^^^^^{-1} A -[[pongA(6)]]-> A
main =
a : A
a = ping (@A {})
# ^^^^ A#ping(5): A -[[pingA(5)]]-> A
a

View file

@ -0,0 +1,22 @@
app "test" provides [main] to "./platform"
Bounce has
ping : a -> a | a has Bounce
pong : a -> a | a has Bounce
A := {} has [Bounce {ping, pong}]
ping = \@A {} -> pong (@A {})
# ^^^^ A#pong(6): A -[[pong(6)]]-> A
#^^^^{-1} A#ping(5): A -[[ping(5)]]-> A
pong = \@A {} -> ping (@A {})
# ^^^^ A#ping(5): A -[[ping(5)]]-> A
#^^^^{-1} A#pong(6): A -[[pong(6)]]-> A
main =
a : A
a = ping (@A {})
# ^^^^ A#ping(5): A -[[ping(5)]]-> A
a

View file

@ -0,0 +1,17 @@
app "test" provides [main] to "./platform"
Diverge has diverge : a -> a | a has Diverge
A := {} has [Diverge {diverge}]
diverge : A -> A
diverge = \@A {} -> diverge (@A {})
# ^^^^^^^ A#diverge(4): A -[[diverge(4)]]-> A
#^^^^^^^{-1} A#diverge(4): A -[[diverge(4)]]-> A
main =
a : A
a = diverge (@A {})
# ^^^^^^^ A#diverge(4): A -[[diverge(4)]]-> A
a

View file

@ -0,0 +1,17 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
Thunk a : {} -> a
Id has id : a -> Thunk a | a has Id
A := {} has [Id {id}]
id = \@A {} -> \{} -> @A {}
#^^{-1} A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})
main =
a : A
a = (id (@A {})) {}
# ^^ A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})
a

View file

@ -0,0 +1,20 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
Thunk a : {} -> a
Id has id : a -> Thunk a | a has Id
A := {} has [Id {id}]
id = \@A {} -> \{} -> @A {}
#^^{-1} A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})
main =
alias = \x -> id x
# ^^ Id#id(3): a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) | a has Id
a : A
a = (alias (@A {})) {}
# ^^^^^ {} -[[alias(9)]]-> ({} -[[8]]-> {})
a

View file

@ -0,0 +1,16 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
Thunk a := {} -> a
Id has id : a -> Thunk a | a has Id
A := {} has [Id {id}]
id = \@A {} -> @Thunk (\{} -> @A {})
#^^{-1} A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})
main =
thunk = id (@A {})
@Thunk it = thunk
it {}
#^^{-1} {} -[[8]]-> {}