-
-
Notifications
You must be signed in to change notification settings - Fork 56
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #638 from bvssvni/ty
Simple refinement types
- Loading branch information
Showing
79 changed files
with
4,009 additions
and
2,223 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
fn foo(a: bool => false, b: bool) -> bool {return a && b} | ||
|
||
fn main() { | ||
println(foo(false, { | ||
println("this is a test") | ||
false | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
fn foo(a: f64 => 0, b: f64) -> f64 {return a * b} | ||
|
||
fn main() { | ||
println(foo(0, { | ||
println("this is a test") | ||
2 | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
fn foo(a: [f64] => [], b: [f64]) -> [f64] {return clone(a)} | ||
|
||
fn main() { | ||
println(foo([], { | ||
println("this is a test") | ||
[1, 2] | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
fn foo(a: str => "hi", b: str) -> str {return clone(a)} | ||
|
||
fn main() { | ||
println(foo("hi", { | ||
println("this is a test") | ||
"hello" | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
fn foo(a: res[str] => ok(_), b: str) -> str {return unwrap_or(a, b)} | ||
|
||
fn main() { | ||
println(foo(ok("hi"), { | ||
println("this is a test") | ||
"hello" | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
fn foo(a: res[str] => ok(_), b: str) -> str {return unwrap_or(a, b)} | ||
|
||
fn main() { | ||
a := ok("hi") | ||
println(foo(a, { | ||
println("this is a test") | ||
"hello" | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
fn foo(a: res[str] => err(_), b: str) -> any { | ||
return if is_err(a) {unwrap_err(a)} | ||
else {clone(b)} | ||
} | ||
|
||
fn main() { | ||
a := err("hi") | ||
println(foo(a, { | ||
println("this is a test") | ||
"hello" | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
fn foo(a: any => ok(_) | some(_), b: str) -> str { | ||
return unwrap_or(a, b) | ||
} | ||
|
||
fn main() { | ||
a := ok("hi") | ||
println(foo(a, { | ||
println("this is a test") | ||
"hello" | ||
})) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
// Must use `sec[bool]` or `sec[f64]`. | ||
fn check(_: sec) {} | ||
|
||
fn main() { | ||
check(explain_where(2, "")) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,6 +1,12 @@ | ||
norm(x: f64) = x+1 | ||
// Use `any` implicitly. | ||
fn foo(x) -> {return x + 1} | ||
// Add simple refinement types to catch more errors. | ||
(f64) -> f64 | ||
(any) -> vec4 | ||
|
||
bar(x: f64) = x + 1 | ||
|
||
fn main() { | ||
a := \(x: f64) = |x| | ||
println(\a(2)) | ||
x := bar(foo((1, 2))) | ||
println(x) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn foo(a: bool) -> {return clone(a)} | ||
(bool, bool) -> bool | ||
|
||
fn main() { | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
fn main() { | ||
println([0; false]) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn foo() -> Foo \() -> bool {return \() = true} | ||
fn main() { | ||
a := foo() | ||
println(\a()) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
fn foo(a) -> {return clone(a)} | ||
(bool) -> bool | ||
(f64) -> f64 | ||
|
||
fn main() { | ||
println(foo("hi")) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
fn foo(a, b) -> {return clone(a)} | ||
(bool, bool) -> bool | ||
(f64, bool) -> f64 | ||
|
||
fn main() { | ||
println(foo(1, 2)) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
fn foo(a) -> {return clone(a)} | ||
(bool) -> bool | ||
(any) -> f64 | ||
|
||
fn main() { | ||
println(foo(1)) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T f64, T f64) -> T f64 } | ||
|
||
fn km(a: f64) -> km f64 {return clone(a)} | ||
|
||
fn check_km(a: km f64) {} | ||
|
||
fn main() { | ||
check_km(foo(km(2), 3)) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T f64, T f64) -> T f64 } | ||
|
||
fn km(a: f64) -> km f64 {return clone(a)} | ||
fn m(a: f64) -> m f64 {return clone(a)} | ||
|
||
fn check_km(a: km f64) {} | ||
|
||
fn main() { | ||
check_km(foo(m(2), km(3))) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T f64, T f64) -> T f64 } | ||
|
||
fn km(a: f64) -> km f64 {return clone(a)} | ||
|
||
fn check_km(a: km f64) {} | ||
|
||
fn main() { | ||
check_km(foo(km(2), km(3))) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T f64, T f64) -> T f64 } | ||
|
||
fn check_f64(a: f64) {} | ||
|
||
fn main() { | ||
check_f64(foo(2, 3)) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T f64, T f64) -> T f64 } | ||
|
||
fn km(a: f64) -> km f64 {return clone(a)} | ||
|
||
fn check_km(a: km f64) {} | ||
|
||
fn main() { | ||
// Allow no ad-hoc type before the first one. | ||
check_km(foo(2, km(3))) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
fn km(a: any) -> km any {return clone(a)} | ||
(vec4) -> km vec4 | ||
(f64) -> km f64 | ||
fn m(a: any) -> m any {return clone(a)} | ||
(vec4) -> m vec4 | ||
(f64) -> m f64 | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T vec4, T vec4) -> T vec4 } | ||
all T { (T vec4, T f64) -> T vec4 } | ||
|
||
fn check_m(a: m vec4) {} | ||
|
||
fn main() { | ||
check_m(foo(m((2, 0)), m(2))) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
fn m(a: any) -> m any {return clone(a)} | ||
(vec4) -> m vec4 | ||
(f64) -> m f64 | ||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T vec4, T vec4) -> T vec4 } | ||
all T { (T vec4, f64) -> T vec4 } | ||
|
||
fn check_m(a: m vec4) {} | ||
|
||
fn main() { | ||
check_m(foo(m((2, 0)), 2)) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
fn km(a: any) -> km any {return clone(a)} | ||
(vec4) -> km vec4 | ||
(f64) -> km f64 | ||
fn m(a: any) -> m any {return clone(a)} | ||
(vec4) -> m vec4 | ||
(f64) -> m f64 | ||
|
||
fn foo(a: any, b: any) -> any {return a + b} | ||
all T { (T f64, T f64) -> T f64 } | ||
all T { (T vec4, T vec4) -> T vec4 } | ||
all T { (T vec4, T f64) -> T vec4 } | ||
(f64, vec4) -> vec4 | ||
|
||
fn check_m(a: m vec4) {} | ||
|
||
fn main() { | ||
check_m(foo(m(2), km((1, 0)))) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn foo(a: bool) -> {return clone(a)} | ||
(str) -> bool | ||
|
||
fn main() { | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
fn foo(a: bool) -> bool {return clone(a)} | ||
(bool) -> str | ||
|
||
fn main() { | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
// Use `any` implicitly. | ||
fn foo(x) -> {return x + 1} | ||
// Add simple refinement types to catch more errors. | ||
(f64) -> f64 | ||
(vec4) -> vec4 | ||
|
||
bar(x: f64) = x + 1 | ||
|
||
fn main() { | ||
x := bar(foo((1, 2))) | ||
println(x) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
fn check_bool(_: bool) {} | ||
fn foo(a) -> {return clone(a)} | ||
([]) -> [bool] | ||
|
||
fn main() { | ||
check_bool(foo([true, true, false])) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
fn check_bool(_: bool) {} | ||
fn foo(a) -> {return clone(a)} | ||
([bool]) -> [bool] | ||
fn bar(a: [bool]) -> [] {return clone(a)} | ||
|
||
fn main() { | ||
// `bar` returns an ambiguous array type `[]`, | ||
// so `foo` should not refine type type, | ||
// which should make `check_bool` not detect a type error. | ||
check_bool(foo(bar([true, true, false]))) | ||
} |
Oops, something went wrong.