-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
6 changed files
with
175 additions
and
55 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| {-# LANGUAGE AllowAmbiguousTypes #-} | ||
|
|
||
| {- | ||
| NOTE [constraint solver addition] | ||
| The functions in this module enable us introduce trivial constraints that are not | ||
| solved by the constraint solver. | ||
| -} | ||
| module Data.Constraint.Nat.Extra where | ||
|
|
||
| import Clash.Prelude | ||
| import Data.Constraint | ||
| import Unsafe.Coerce (unsafeCoerce) | ||
|
|
||
| {- | Postulates that multiplying some number /a/ by some constant /b/, and | ||
| subsequently dividing that result by /b/ equals /a/. | ||
| -} | ||
| cancelMulDiv :: forall a b. (1 <= b) => Dict (DivRU (a * b) b ~ a) | ||
| cancelMulDiv = unsafeCoerce (Dict :: Dict (0 ~ 0)) | ||
|
|
||
| -- | if (1 <= b) then (Mod a b + 1 <= b) | ||
| leModulusDivisor :: forall a b. 1 <= b => Dict (Mod a b + 1 <= b) | ||
| leModulusDivisor = unsafeCoerce (Dict :: Dict (0 <= 0)) | ||
|
|
||
| -- | if (a <= 0) then (a ~ 0) | ||
| leZeroIsZero :: forall a. (a <= 0) => Dict (a ~ 0) | ||
| leZeroIsZero = unsafeCoerce (Dict :: Dict (0 ~ 0)) | ||
|
|
||
| -- | if (1 <= a) and (1 <= b) then (1 <= DivRU a b) | ||
| strictlyPositiveDivRu :: forall a b. (1 <= a, 1 <= b) => Dict (1 <= DivRU a b) | ||
| strictlyPositiveDivRu = unsafeCoerce (Dict :: Dict (0 <= 0)) | ||
|
|
||
| -- | if (1 <= a) then (b <= ceiling(b/a) * a) | ||
| timesDivRu :: forall a b. (1 <= a) => Dict (b <= Div (b + (a - 1)) a * a) | ||
| timesDivRu = unsafeCoerce (Dict :: Dict (0 <= 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
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,99 @@ | ||
| {-# LANGUAGE NumericUnderscores #-} | ||
|
|
||
| module Tests.Haxioms where | ||
|
|
||
| import Prelude | ||
| import Numeric.Natural | ||
|
|
||
| import Hedgehog | ||
| import qualified Hedgehog.Gen as Gen | ||
| import qualified Hedgehog.Range as Range | ||
|
|
||
| import Test.Tasty | ||
| import Test.Tasty.Hedgehog (HedgehogTestLimit (HedgehogTestLimit)) | ||
| import Test.Tasty.Hedgehog.Extra (testProperty) | ||
| import Test.Tasty.TH (testGroupGenerator) | ||
|
|
||
| -- | Generate a 'Natural' greater than or equal to /n/. Can generate 'Natural's | ||
| -- up to /n+1000/. This should be enough, given that naturals in this module are | ||
| -- used in proofs. | ||
| genNatural :: Natural -> Gen Natural | ||
| genNatural min_ = Gen.integral (Range.linear min_ (1000 + min_)) | ||
|
|
||
| -- | Like 'DivRU', but at term-level. | ||
| divRU :: Natural -> Natural -> Natural | ||
| divRU dividend divider = | ||
| case dividend `divMod` divider of | ||
| (n, 0) -> n | ||
| (n, _) -> n + 1 | ||
|
|
||
| -- | Test whether the following equation holds: | ||
| -- | ||
| -- DivRU (a * b) b ~ a | ||
| -- | ||
| -- Given: | ||
| -- | ||
| -- 1 <= b | ||
| -- | ||
| -- Tests: 'Data.Constraint.Nat.Extra.cancelMulDiv'. | ||
| -- | ||
| prop_cancelMulDiv :: Property | ||
| prop_cancelMulDiv = property $ do | ||
| a <- forAll (genNatural 0) | ||
| b <- forAll (genNatural 1) | ||
| divRU (a * b) b === a | ||
|
|
||
| -- | Test whether the following equation holds: | ||
| -- | ||
| -- Mod a b + 1 <= b | ||
| -- | ||
| -- Given: | ||
| -- | ||
| -- 1 <= b | ||
| -- | ||
| -- Tests: 'Data.Constraint.Nat.Extra.leModulusDivisor'. | ||
| -- | ||
| prop_leModulusDivisor :: Property | ||
| prop_leModulusDivisor = property $ do | ||
| a <- forAll (genNatural 0) | ||
| b <- forAll (genNatural 1) | ||
| assert (a `mod` b + 1 <= b) | ||
|
|
||
| -- | Test whether the following equation holds: | ||
| -- | ||
| -- 1 <= DivRU a b | ||
| -- | ||
| -- Given: | ||
| -- | ||
| -- 1 <= a, 1 <= b | ||
| -- | ||
| -- Tests: 'Data.Constraint.Nat.Extra.strictlyPositiveDivRu'. | ||
| -- | ||
| prop_strictlyPositiveDivRu :: Property | ||
| prop_strictlyPositiveDivRu = property $ do | ||
| a <- forAll (genNatural 1) | ||
| b <- forAll (genNatural 1) | ||
| assert (1 <= divRU a b) | ||
|
|
||
| -- | Test whether the following equation holds: | ||
| -- | ||
| -- b <= Div (b + (a - 1)) a * a | ||
| -- | ||
| -- Given: | ||
| -- | ||
| -- 1 <= a | ||
| -- | ||
| -- Tests: 'Data.Constraint.Nat.Extra.timesDivRU'. | ||
| -- | ||
| prop_timesDivRU :: Property | ||
| prop_timesDivRU = property $ do | ||
| a <- forAll (genNatural 1) | ||
| b <- forAll (genNatural 0) | ||
| assert (b <= (b + (a - 1) `div` a) * a) | ||
|
|
||
| tests :: TestTree | ||
| tests = | ||
| localOption (mkTimeout 10_000_000 {- 10 seconds -}) $ | ||
| localOption | ||
| (HedgehogTestLimit (Just 100_000)) | ||
| $(testGroupGenerator) |
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