Skip to content

Commit

Permalink
renaming
Browse files Browse the repository at this point in the history
  • Loading branch information
@stefan-aws
stefan-aws committed Nov 6, 2023
1 parent c85a906 commit 3c4ebf0
Show file tree
Hide file tree
Showing 6 changed files with 20 additions and 20 deletions.
2 changes: 1 addition & 1 deletion docs/dafny/ExamplesExternUniform.dfy → ...dafny/ExamplesExternUniformPowerOfTwo.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ module RandomExamples.ExternUniform {
decreases *
{
var n := 100000;
var r: DafnyVMC.DRandomExternUniform := new DafnyVMC.DRandomExternUniform();
var r: DafnyVMC.DRandomExternUniformPowerOfTwo := new DafnyVMC.DRandomExternUniformPowerOfTwo();

var t := 0;
for i := 0 to n {
Expand Down
2 changes: 1 addition & 1 deletion scripts/build.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,4 @@ then
exit 1
fi

$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify
$DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG src/Dafny-VMC.dfy -o build/$TARGET_LANG/Dafny-VMC dfyconfig.toml --no-verify
16 changes: 8 additions & 8 deletions scripts/test.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,14 +16,14 @@ fi

echo Running $TARGET_LANG tests...
echo "Running tests/TestsFoundational.dfy:"
time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsFoundational.dfy tests/Tests.dfy dfyconfig.toml --no-verify
echo "Running tests/TestsExternUniform.dfy:"
time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG tests/TestsExternUniform.dfy tests/Tests.dfy dfyconfig.toml --no-verify
time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG tests/TestsExternUniformPowerOfTwo.dfy tests/Tests.dfy dfyconfig.toml --no-verify

echo Running $TARGET_LANG documentation...

echo "Building docs/dafny/ExamplesFoundational.dfy..."
$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG dfyconfig.toml --no-verify
$DAFNY build docs/dafny/ExamplesFoundational.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
echo "Executing compiled docs/dafny/ExamplesFoundational.dfy:"
if [ "$TARGET_LANG" = "cs" ]
then
Expand All @@ -32,12 +32,12 @@ else
java -jar docs/dafny/ExamplesFoundational.jar
fi

echo "Building docs/dafny/ExamplesExternUniform.dfy..."
$DAFNY build docs/dafny/ExamplesExternUniform.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniform.$TARGET_LANG dfyconfig.toml --no-verify
echo "Executing compiled docs/dafny/ExamplesExternUniform.dfy:"
echo "Building docs/dafny/ExamplesExternUniformPowerOfTwo.dfy..."
$DAFNY build docs/dafny/ExamplesExternUniformPowerOfTwo.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/DRandomCoin.$TARGET_LANG src/interop/$TARGET_LANG/DRandomUniformPowerOfTwo.$TARGET_LANG dfyconfig.toml --no-verify
echo "Executing compiled docs/dafny/ExamplesExternUniformPowerOfTwo.dfy:"
if [ "$TARGET_LANG" = "cs" ]
then
dotnet docs/dafny/ExamplesExternUniform.dll
dotnet docs/dafny/ExamplesExternUniformPowerOfTwo.dll
else
java -jar docs/dafny/ExamplesExternUniform.jar
java -jar docs/dafny/ExamplesExternUniformPowerOfTwo.jar
fi
2 changes: 1 addition & 1 deletion src/Dafny-VMC.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module DafnyVMC {
constructor {:extern} ()
}

class DRandomExternUniform extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.TraitExtern, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitFoundational, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
class DRandomExternUniformPowerOfTwo extends Coin.Interface.Trait, UniformPowerOfTwo.Implementation.TraitExtern, Bernoulli.Implementation.Trait, Uniform.Implementation.TraitFoundational, BernoulliExpNeg.Implementation.Trait, DiscreteGaussian.Implementation.Trait, DiscreteLaplace.Implementation.Trait {
constructor {:extern} ()
}
}
0 src/interop/java/DRandomUniform.java → ...nterop/java/DRandomUniformPowerOfTwo.java
View file
File renamed without changes.
18 changes: 9 additions & 9 deletions tests/TestsExternUniform.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,63 +8,63 @@ module TestsExternUniform {
import Tests

method {:test} TestCoin() {
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestCoin(1_000_000, r);
}

method {:test} TestUniform()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestUniform(1_000_000, r);
}

method {:test} TestUniformInterval()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestUniformInterval(1_000_000, r);
}

method {:test} TestBernoulli()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestBernoulli(1_000_000, r);
}

method {:test} TestBernoulli2()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestBernoulli2(1_000_000, r);
}

method {:test} TestBernoulli3()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestBernoulli3(1_000_000, r);
}

method {:test} TestBernoulliExpNeg()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestBernoulliExpNeg(1_000_000, r);
}

method {:test} TestDiscreteLaplace()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestDiscreteLaplace(1_000_000, r);
}

method {:test} TestDiscreteGaussian()
decreases *
{
var r := new DafnyVMC.DRandomExternUniform();
var r := new DafnyVMC.DRandomExternUniformPowerOfTwo();
Tests.TestDiscreteGaussian(1_000_000, r);
}
}

0 comments on commit 3c4ebf0

Please sign in to comment.