Skip to content

Chore: Rust refactorings #5786

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.

Sign up for GitHub

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

Merged
merged 11 commits into from
Sep 24, 2024
Merged

Chore: Rust refactorings #5786

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
f135054
Almost only refactorings
MikaelMayer Sep 18, 2024
dde7963
Tried to fix a bug in new resolver but still not working.
MikaelMayer Sep 20, 2024
1ed7e04
Merge branch 'master' into chore-refactorings
MikaelMayer Sep 23, 2024
b4f0dda
regenerated files
MikaelMayer Sep 24, 2024
239c5e6
Merge branch 'master' into chore-refactorings
MikaelMayer Sep 24, 2024
c63193a
Added missing Defs file
MikaelMayer Sep 24, 2024
ad948e5
format
MikaelMayer Sep 24, 2024
237d5cc
fixed CI test
MikaelMayer Sep 24, 2024
6cf4c37
Merge branch 'master' into chore-refactorings
MikaelMayer Sep 24, 2024
d579aa9
Removed equality feature as it's incomplete.
MikaelMayer Sep 24, 2024
5dd631d
Regenerated files
MikaelMayer Sep 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
# Run these tasks even if eponymous files or folders exist
.PHONY: test-dafny exe

DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))

default: exe
Expand Down Expand Up @@ -30,6 +33,24 @@ tests:
test:
(cd "${DIR}"; dotnet test Source/IntegrationTests --filter "DisplayName~${name}")

# Run Dafny on an integration test case directly in the folder itself.
# make test-run name=<part of the path> action="run ..."
test-dafny:
name="$(name)"; \
files=$$(cd "${DIR}"/Source/IntegrationTests/TestFiles/LitTests/LitTest; find . -type f -wholename "*$$name*" | grep -E '\.dfy$$'); \
count=$$(echo "$$files" | wc -l); \
echo "$${files}"; \
if [ "$$count" -eq 0 ]; then \
echo "No files found matching pattern: $$name"; \
exit 1; \
else \
echo "$$count test files found."; \
for file in $$files; do \
filedir=$$(dirname "$$file"); \
(cd "${DIR}/Source/IntegrationTests/TestFiles/LitTests/LitTest/$${filedir}"; "${DIR}"/Binaries/Dafny $(action) "$$(basename $$file)" ); \
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not blocking since this doesn't appear to be used for any automation, but I would suggest using dotnet run ... instead of Binaries/Dafny to prevent the mistake of running make test-run ... on an outdated binary.

done; \
fi

tests-verbose:
(cd "${DIR}"; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -737,7 +737,7 @@ protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, C
}

public override string TailRecursiveVar(int inParamIndex, IVariable variable) {
return preventShadowing ? base.TailRecursiveVar(inParamIndex, variable) : DCOMP.COMP.TailRecursionPrefix.ToVerbatimString(false) + inParamIndex;
return preventShadowing ? base.TailRecursiveVar(inParamIndex, variable) : Defs.__default.TailRecursionPrefix.ToVerbatimString(false) + inParamIndex;
}

protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
Expand Down Expand Up @@ -998,7 +998,7 @@ protected override void EmitStaticExternMethodQualifier(string qual, ConcreteSyn
if (GetExprBuilder(wr, out var builder)) {
builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_ExternCompanion(
Sequence<ISequence<Rune>>.FromArray(new[] {
DCOMP.COMP.DAFNY__EXTERN__MODULE,
Defs.__default.DAFNY__EXTERN__MODULE,
Sequence<Rune>.UnicodeFromString(qual)
})
));
Expand Down
Loading