Skip to content
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

Prepare 0.2.1.0 release #4

Merged
merged 1 commit into from
Feb 3, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions .github/CODEOWNERS
Validating CODEOWNERS rules …
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
@byteverse/l3c
12 changes: 12 additions & 0 deletions .github/workflows/build.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
name: build
on:
pull_request:
branches:
- "*"

jobs:
call-workflow:
uses: byteverse/.github/.github/workflows/build.yaml@main
secrets: inherit
with:
release: false
12 changes: 12 additions & 0 deletions .github/workflows/release.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
name: release
on:
push:
tags:
- "*"

jobs:
call-workflow:
uses: byteverse/.github/.github/workflows/build.yaml@main
secrets: inherit
with:
release: true
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
.vscode/
dist
dist-*
cabal-dev
Expand Down
3 changes: 2 additions & 1 deletion CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
# Revision history for natural-arithmetic

## 0.2.1.0 -- 2024-??-??
## 0.2.1.0 -- 2024-02-02

* Add `fromInt` and `fromInt#` to `Arithmetic.Fin`.
* Update package metadata.

## 0.2.0.0 -- 2024-01-09

Expand Down
2 changes: 0 additions & 2 deletions Setup.hs

This file was deleted.

51 changes: 51 additions & 0 deletions fourmolu.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
# Number of spaces per indentation step
indentation: 2

# Max line length for automatic line breaking
column-limit: 200

# Styling of arrows in type signatures (choices: trailing, leading, or leading-args)
function-arrows: trailing

# How to place commas in multi-line lists, records, etc. (choices: leading or trailing)
comma-style: leading

# Styling of import/export lists (choices: leading, trailing, or diff-friendly)
import-export-style: leading

# Whether to full-indent or half-indent 'where' bindings past the preceding body
indent-wheres: false

# Whether to leave a space before an opening record brace
record-brace-space: true

# Number of spaces between top-level declarations
newlines-between-decls: 1

# How to print Haddock comments (choices: single-line, multi-line, or multi-line-compact)
haddock-style: multi-line

# How to print module docstring
haddock-style-module: null

# Styling of let blocks (choices: auto, inline, newline, or mixed)
let-style: auto

# How to align the 'in' keyword with respect to the 'let' keyword (choices: left-align, right-align, or no-space)
in-style: right-align

# Whether to put parentheses around a single constraint (choices: auto, always, or never)
single-constraint-parens: always

# Output Unicode syntax (choices: detect, always, or never)
unicode: never

# Give the programmer more choice on where to insert blank lines
respectful: true

# Fixity information for operators
fixities: []

# Module reexports Fourmolu should know about
reexports: []

55 changes: 33 additions & 22 deletions natural-arithmetic.cabal
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
cabal-version: 2.2
name: natural-arithmetic
version: 0.2.1.0
synopsis: Arithmetic of natural numbers
cabal-version: 2.2
name: natural-arithmetic
version: 0.2.1.0
synopsis: Arithmetic of natural numbers
description:
A search for terms like `arithmetic` and `natural` on hackage reveals
no shortage of libraries for handling the arithmetic of natural
Expand All @@ -18,7 +18,7 @@ description:
application code, not in library code. This is because libraries
should not require the presence of typechecker plugins. Technically,
they can (you could document it), but many developers will not
use libraries that have unusual install procedures like this.
use libraries that have unusual install procedures like this.
.
This library, in places, requires users to use the 'TypeApplications`
language extension. This is done when a number is only need at
Expand All @@ -28,7 +28,7 @@ description:
in `Arithmetic.Lt` and `Arithmetic.Lte`. This is done in the interest
of making it easy for user to assemble proofs. Recall that proof
assembly is done by hand rather than by an SMT solver, so removing
some tediousness from this is helpful to users.
some tediousness from this is helpful to users.
.
This library provides left and variants variants of several functions.
For example, `Arithmetic.Lte` provides both `substituteL` and
Expand All @@ -54,29 +54,40 @@ description:
* Decrement: Decrease an upper bound along with the bounded value
.
* Substitute: Replace a number with an equal number
homepage: https://github.com/andrewthad/natural-arithmetic
bug-reports: https://github.com/andrewthad/natural-arithmetic/issues
license: BSD-3-Clause
license-file: LICENSE
author: Andrew Martin
maintainer: [email protected]
copyright: 2019 Andrew Martin
category: Math
extra-source-files: CHANGELOG.md

homepage: https://github.com/byteverse/natural-arithmetic
bug-reports: https://github.com/byteverse/natural-arithmetic/issues
license: BSD-3-Clause
license-file: LICENSE
author: Andrew Martin
maintainer: [email protected]
copyright: 2019 Andrew Martin
category: Math
extra-doc-files: CHANGELOG.md

common build-settings
default-language: Haskell2010
ghc-options: -Wall -Wunused-packages

library
import: build-settings
exposed-modules:
Arithmetic.Fin
Arithmetic.Equal
Arithmetic.Fin
Arithmetic.Lt
Arithmetic.Lte
Arithmetic.Nat
Arithmetic.Plus
Arithmetic.Types
Arithmetic.Unsafe
Arithmetic.Plus

build-depends:
, base>=4.14 && <5
, unlifted >=0.2.1
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall -O2
, base >=4.14 && <5
, unlifted >=0.2.1

hs-source-dirs: src
ghc-options: -O2

source-repository head
type: git
location: git://github.com/byteverse/natural-arithmetic.git
26 changes: 13 additions & 13 deletions src/Arithmetic/Equal.hs
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
{-# language DataKinds #-}
{-# language ExplicitForAll #-}
{-# language KindSignatures #-}
{-# language MagicHash #-}
{-# language TypeOperators #-}
{-# language UnboxedTuples #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}

module Arithmetic.Equal
( symmetric
Expand All @@ -14,29 +14,29 @@ module Arithmetic.Equal
, lift
) where

import Arithmetic.Unsafe (type (:=:)(Eq), type (:=:#)(Eq#))
import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#))
import GHC.TypeNats (type (+))

symmetric :: (m :=: n) -> (n :=: m)
{-# inline symmetric #-}
{-# INLINE symmetric #-}
symmetric Eq = Eq

plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)
{-# inline plusL #-}
{-# INLINE plusL #-}
plusL Eq = Eq

plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)
{-# inline plusR #-}
{-# INLINE plusR #-}
plusR Eq = Eq

plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n)
{-# inline plusL# #-}
{-# INLINE plusL# #-}
plusL# _ = Eq# (# #)

plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c)
{-# inline plusR# #-}
{-# INLINE plusR# #-}
plusR# _ = Eq# (# #)

lift :: (m :=:# n) -> (m :=: n)
{-# inline lift #-}
{-# INLINE lift #-}
lift _ = Eq
Loading
Loading