Skip to content
Permalink
Browse files

Small improvements for Prelude.Natural (#719)

* Add Natural.subtract

* Small improvements for the Natural comparison functions
  - Add property assertions
  - Only lessThanEqual uses the Natural/subtract primitive, everything
    else is ultimately implemented in terms of lessThanEqual.
  - greaterThanEqual now requires only 2 normalization steps instead of 3

* Update nixops/dhall-haskell.json
  Command used:

    nix-prefetch-git --fetch-submodules https://github.com/dhall-lang/dhall-haskell
  • Loading branch information...
sjakobi committed Sep 6, 2019
1 parent 11eab49 commit 898510cfb85bc6bf9bf80ba8739a2f07f02f19ca
@@ -1,15 +1,18 @@
{-
`equal` checks if two Naturals are equal.
-}
let lessThanEqual =
./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
? ./lessThanEqual

let equal
: Natural Natural Bool
= λ(a : Natural)
λ(b : Natural)
Natural/isZero (Natural/subtract a b)
&& Natural/isZero (Natural/subtract b a)
= λ(a : Natural) λ(b : Natural) lessThanEqual a b && lessThanEqual b a

let example0 = assert : equal 5 5 True

let example1 = assert : equal 5 6 False

let property0 = λ(n : Natural) assert : equal n n True

in equal
@@ -1,23 +1,22 @@
{-
`greaterThan` checks if one Natural is strictly greater than another.
-}

let Bool/not =
../Bool/not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
? ../Bool/not

let lessThanEqual =
./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
? ./lessThanEqual
let lessThan =
./lessThan sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c
? ./lessThan

let greaterThan
: Natural Natural Bool
= λ(x : Natural) λ(y : Natural) Bool/not (lessThanEqual x y)
= λ(x : Natural) λ(y : Natural) lessThan y x

let example0 = assert : greaterThan 5 6 False

let example1 = assert : greaterThan 5 5 False

let example2 = assert : greaterThan 5 4 True

let property0 = λ(n : Natural) assert : greaterThan 0 n False

let property1 = λ(n : Natural) assert : greaterThan n n False

in greaterThan
@@ -1,22 +1,22 @@
{-
`greaterThanEqual` checks if one Natural is greater than or equal to another.
-}
let Bool/not =
../Bool/not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
? ../Bool/not

let lessThan =
./lessThan sha256:d8a37951fd3f88dcc3927c20b73e6c53499f5275d949eed59bb77ea748492bf0
? ./lessThan
let lessThanEqual =
./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
? ./lessThanEqual

let greaterThanEqual
: Natural Natural Bool
= λ(x : Natural) λ(y : Natural) Bool/not (lessThan x y)
= λ(x : Natural) λ(y : Natural) lessThanEqual y x

let example0 = assert : greaterThanEqual 5 6 False

let example1 = assert : greaterThanEqual 5 5 True

let example1 = assert : greaterThanEqual 5 4 True
let example2 = assert : greaterThanEqual 5 4 True

let property0 = λ(n : Natural) assert : greaterThanEqual n 0 True

let property1 = λ(n : Natural) assert : greaterThanEqual n n True

in greaterThanEqual
@@ -1,23 +1,26 @@
{-
`lessThan` checks if one Natural is strictly less than another.
Examples:
```
```
-}
let lessThanEqual =
./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
? ./lessThanEqual
let greaterThanEqual =
./greaterThanEqual sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4
? ./greaterThanEqual

let Bool/not =
../Bool/not sha256:723df402df24377d8a853afed08d9d69a0a6d86e2e5b2bac8960b0d4756c7dc4
? ../Bool/not

let lessThan
: Natural Natural Bool
= λ(x : Natural) λ(y : Natural) lessThanEqual (x + 1) y
= λ(x : Natural) λ(y : Natural) Bool/not (greaterThanEqual x y)

let example0 = assert : lessThan 5 6 True

let example1 = assert : lessThan 5 5 False

let example2 = assert : lessThan 5 4 False

let property0 = λ(n : Natural) assert : lessThan n 0 False

let property1 = λ(n : Natural) assert : lessThan n n False

in lessThan
@@ -1,4 +1,3 @@

{-
`lessThanEqual` checks if one Natural is less than or equal to another.
-}
@@ -12,4 +11,8 @@ let example1 = assert : lessThanEqual 5 5 ≡ True

let example2 = assert : lessThanEqual 5 4 False

let property0 = λ(n : Natural) assert : lessThanEqual 0 n True

let property1 = λ(n : Natural) assert : lessThanEqual n n True

in lessThanEqual
@@ -32,18 +32,21 @@
./toInteger sha256:160d2d278619f3da34a1f4f02e739a447e4f2aa5a2978c45b710515b41491e1f
? ./toInteger
, lessThan =
./lessThan sha256:d8a37951fd3f88dcc3927c20b73e6c53499f5275d949eed59bb77ea748492bf0
./lessThan sha256:3381b66749290769badf8855d8a3f4af62e8de52d1364d838a9d1e20c94fa70c
? ./lessThan
, lessThanEqual =
./lessThanEqual sha256:1a5caa2b80a42b9f58fff58e47ac0d9a9946d0b2d36c54034b8ddfe3cb0f3c99
? ./lessThanEqual
, equal =
./equal sha256:9e0e952e097a2a974ca4ed3e65bcf395cda2bb54382c8ecc3963bca50bfff124
./equal sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
? ./equal
, greaterThanEqual =
./greaterThanEqual sha256:8665ab478524416ecca7573488eb9b64c12a39f1ea86353b67735cf4d3a3bc4f
./greaterThanEqual sha256:30ebfab0febd7aa0ccccfdf3dc36ee6d50f0117f35dd4a9b034750b7e885a1a4
? ./greaterThanEqual
, greaterThan =
./greaterThan sha256:f702abcdfcd7ad73619b9285d7e41c3a1d017fb6b8d037cf40bd93bf30c09b2c
? ./greaterThan
, subtract =
./subtract sha256:b9277ac637d09142a3a3ac79137ef5955c42f8b33b6746d59db2c9d75ccdd745
? ./subtract
}
@@ -0,0 +1,18 @@
{-
`subtract m n` computes `n - m`, truncating to `0` if `m > n`
-}
let subtract : Natural Natural Natural = Natural/subtract

let example0 = assert : subtract 1 2 1

let example1 = assert : subtract 1 1 0

let example2 = assert : subtract 2 1 0

let property0 = λ(n : Natural) assert : subtract 0 n n

let property1 = λ(n : Natural) assert : subtract n 0 0

let property2 = λ(n : Natural) assert : subtract n n 0

in subtract
@@ -17,7 +17,7 @@
./Map/package.dhall sha256:07cc274220c8bdb2c1a0c2d00d90bc1447e73e0ad2e1d72b89773e923f77e71e
? ./Map/package.dhall
, Natural =
./Natural/package.dhall sha256:8421079b9698b765774455b63f4561f7bfa1506ed3fa39cfb5c34a4cd1c9df4b
./Natural/package.dhall sha256:4574df29e6bb82fd894c311f6c2ad9a22574756eb62f06d475aa8306d25006fc
? ./Natural/package.dhall
, Optional =
./Optional/package.dhall sha256:36a366af67a3c26cd5d196e095d3023f18953c5b5db3a03956fa554609e5442a
@@ -1,7 +1,7 @@
{
"url": "https://github.com/dhall-lang/dhall-haskell.git",
"rev": "2cf6a1ba74e02a3e16a8060cacba026c66e2ff23",
"date": "2019-08-03T21:38:01-07:00",
"sha256": "0ilp0dhfvbjzx8wh27lpijn53ghzjrq8f5cqpfgxiww3n8zliyc9",
"url": "https://github.com/dhall-lang/dhall-haskell",
"rev": "350b54c43ed0914200722e9ab78dfed854771a72",
"date": "2019-09-01T18:09:28+00:00",
"sha256": "0lr0q5jfqsx0j184s9xydzibcp370hikbim0m6dvj50xvf22a4gp",
"fetchSubmodules": true
}

0 comments on commit 898510c

Please sign in to comment.
You can’t perform that action at this time.