-
Notifications
You must be signed in to change notification settings - Fork 400
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Propagate unsafety to definitions that depend on unsafe definitions #379
Changes from 8 commits
e6c8123
bc870fc
3fd3412
55b6b4c
77f8b73
2bfbd99
607426d
0f44d07
0f675a8
92773fb
e016d7c
23ad6dc
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
@List/Cons = (a (b ((@List/Cons/tag (a (b c))) c))) | ||
|
||
@List/Cons/tag = 1 | ||
|
||
@List/Nil = ((@List/Nil/tag a) a) | ||
|
||
@List/Nil/tag = 0 | ||
|
||
@id = (a a) | ||
|
||
@list = c | ||
& @List/Cons ~ (1 (b c)) | ||
& @List/Cons ~ (2 (@List/Nil b)) | ||
|
||
@main = b | ||
& @map ~ (@main__C0 (a b)) | ||
& @List/Cons ~ (@id (@List/Nil a)) | ||
|
||
@main__C0 = (a b) | ||
& @map ~ (a (@list b)) | ||
|
||
@map = (a ((@map__C1 (a b)) b)) | ||
|
||
@map__C0 = (* (a (d ({(a b) c} f)))) | ||
& @List/Cons ~ (b (e f)) | ||
& @map ~ (c (d e)) | ||
|
||
@map__C1 = (?(((* @List/Nil) @map__C0) a) a) | ||
|
||
// Test flags | ||
@test-rust-only = 1 |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -45,6 +45,11 @@ fn test_file(path: &Path) { | |
let rust_output = execute_hvm(&["run".as_ref(), path.as_os_str()], false).unwrap(); | ||
assert_snapshot!(rust_output); | ||
|
||
if contents.contains("@test-rust-only = 1") { | ||
println!("only testing rust implementation for {path:?}"); | ||
return; | ||
} | ||
|
||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I added the possibility to only run tests in the Rust implementation, since the C one doesn't throw an error in this same case. This is something to discuss - should the C and CUDA implementations also "panic" printing this error and stopping the program? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this is fine as is, and is in line with the other |
||
println!(" testing {path:?}, C..."); | ||
let c_output = execute_hvm(&["run-c".as_ref(), path.as_os_str()], false).unwrap(); | ||
assert_eq!(c_output, rust_output, "{path:?}: C output does not match rust output"); | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
--- | ||
source: tests/run.rs | ||
expression: rust_output | ||
input_file: tests/programs/safety-check.hvm | ||
--- | ||
ERROR: attempt to clone a non-affine global reference. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Writing a recursive function like this may not be the best idea since we still don't have a way to increase stack size as needed like in the
hvm-64
repo. I think it's fine for now to add this function like this, since pretty much all the other functions related to trees are also recursive and if this one fails, they do too.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
if it becomes a problem we can just write this imperatively
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This function is quadratic, due to repeatedly cloning these btreesets;
(@a (@b (@c (@d (@e ...)))))
will take triangular time (which is asymptotically quadratic).There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! I thought it would be similar to merging in merge sort, but I tested it and it really is slow. It should be better now.