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.

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

Jump to bottom

[ cleanup ] Make Nat's NonZero to be an alias for IsSucc #3405

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
+30 −21
Open

[ cleanup ] Make Nat's NonZero to be an alias for IsSucc #3405

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 4 additions & 0 deletions CHANGELOG_NEXT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,6 +225,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO

* Added `Data.IORef.atomically` for the chez backend.

* `Data.Nat.NonZero` was made to be an alias for `Data.Nat.IsSucc`.
`SIsNonZero` was made to be an alias for `ItIsSucc`, was marked as deprecated,
and won't work on LHS anymore.

#### Contrib

* `Data.List.Lazy` was moved from `contrib` to `base`.
Expand Down
31 changes: 18 additions & 13 deletions libs/base/Data/Nat.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,9 @@ isSucc : Nat -> Bool
isSucc Z = False
isSucc (S n) = True

||| A definition of non-zero with a better behaviour than `Not (x = Z)`
||| This is amenable to proof search and `NonZero Z` is more readily
||| detected as impossible by Idris
public export
data IsSucc : (n : Nat) -> Type where
ItIsSucc : IsSucc (S n)
Expand All @@ -45,6 +48,17 @@ isItSucc : (n : Nat) -> Dec (IsSucc n)
isItSucc Z = No absurd
isItSucc (S n) = Yes ItIsSucc

||| A hystorical synonym for `IsSucc`
public export
0 NonZero : Nat -> Type
NonZero = IsSucc

-- Remove as soon as 0.8.0 (or greater) is released
public export %inline
%deprecate -- use ItIsSucc instead
SIsNonZero : NonZero (S n)
SIsNonZero = ItIsSucc

public export
power : Nat -> Nat -> Nat
power base Z = S Z
Expand Down Expand Up @@ -319,15 +333,6 @@ export
Injective S where
injective Refl = Refl

||| A definition of non-zero with a better behaviour than `Not (x = Z)`
||| This is amenable to proof search and `NonZero Z` is more readily
||| detected as impossible by Idris
public export
data NonZero : Nat -> Type where
SIsNonZero : NonZero (S x)

export Uninhabited (NonZero Z) where uninhabited SIsNonZero impossible

export
SIsNotZ : Not (S x = Z)
SIsNotZ = absurd
Expand All @@ -351,7 +356,7 @@ modNatNZ left (S right) _ = mod' left left right

export partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNonZero
modNat left (S right) = modNatNZ left (S right) ItIsSucc

||| Auxiliary function:
||| div' fuel a b = a `div` (S b)
Expand All @@ -372,7 +377,7 @@ divNatNZ left (S right) _ = div' left left right

export partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNonZero
divNat left (S right) = divNatNZ left (S right) ItIsSucc

export
covering
Expand All @@ -383,7 +388,7 @@ divCeilNZ x y p = case (modNatNZ x y p) of

export partial
divCeil : Nat -> Nat -> Nat
divCeil x (S y) = divCeilNZ x (S y) SIsNonZero
divCeil x (S y) = divCeilNZ x (S y) ItIsSucc


public export
Expand Down Expand Up @@ -411,7 +416,7 @@ covering
gcd : (a: Nat) -> (b: Nat) -> {auto 0 ok: NotBothZero a b} -> Nat
gcd a Z = a
gcd Z b = b
gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNonZero)
gcd a (S b) = gcd (S b) (modNatNZ a (S b) ItIsSucc)

export partial
lcm : Nat -> Nat -> Nat
Expand Down
8 changes: 4 additions & 4 deletions libs/contrib/Data/Nat/Factor.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,8 +373,8 @@ selfIsCommonFactor a = CommonFactorExists a reflexive reflexive
gcdUnproven' : (m, n : Nat) -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m) -> Nat
gcdUnproven' m Z _ _ = m
gcdUnproven' m (S n) (Access rec) n_lt_m =
let mod_lt_n = boundModNatNZ m (S n) SIsNonZero in
gcdUnproven' (S n) (modNatNZ m (S n) SIsNonZero) (rec _ n_lt_m) mod_lt_n
let mod_lt_n = boundModNatNZ m (S n) ItIsSucc in
gcdUnproven' (S n) (modNatNZ m (S n) ItIsSucc) (rec _ n_lt_m) mod_lt_n

||| Total definition of the gcd function. Does not return GСD evidence, but is faster.
gcdUnproven : Nat -> Nat -> Nat
Expand All @@ -388,7 +388,7 @@ gcdUnproven'Greatest : {m, n, c : Nat} -> (0 sizeM : SizeAccessible m) -> (0 n_l
-> Factor c m -> Factor c n -> Factor c (gcdUnproven' m n sizeM n_lt_m)
gcdUnproven'Greatest {n = Z} _ _ cFactM _ = cFactM
gcdUnproven'Greatest {n = S n} (Access rec) n_lt_m cFactM cFactN =
gcdUnproven'Greatest (rec _ n_lt_m) (boundModNatNZ m (S n) SIsNonZero) cFactN (commonFactorAlsoFactorOfMod cFactM cFactN)
gcdUnproven'Greatest (rec _ n_lt_m) (boundModNatNZ m (S n) ItIsSucc) cFactN (commonFactorAlsoFactorOfMod cFactM cFactN)

gcdUnprovenGreatest : (m, n : Nat) -> {auto 0 ok : NotBothZero m n} -> (q : Nat) -> CommonFactor q m n -> Factor q (gcdUnproven m n)
gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) with (isLT n m)
Expand All @@ -402,7 +402,7 @@ gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) with (isLT n m)

gcdUnproven'CommonFactor : {m, n : Nat} -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m) -> CommonFactor (gcdUnproven' m n sizeM n_lt_m) m n
gcdUnproven'CommonFactor {n = Z} _ _ = CommonFactorExists _ reflexive (anythingFactorZero m)
gcdUnproven'CommonFactor {n = S n} (Access rec) n_lt_m with (gcdUnproven'CommonFactor (rec _ n_lt_m) (boundModNatNZ m (S n) SIsNonZero))
gcdUnproven'CommonFactor {n = S n} (Access rec) n_lt_m with (gcdUnproven'CommonFactor (rec _ n_lt_m) (boundModNatNZ m (S n) ItIsSucc))
gcdUnproven'CommonFactor (Access rec) n_lt_m | (CommonFactorExists _ factM factN)
= CommonFactorExists _ (modFactorAlsoFactorOfDivider factM factN) factM

Expand Down
6 changes: 3 additions & 3 deletions libs/contrib/Data/Vect/Properties/Fin.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,13 +19,13 @@ etaCons (x :: xs) = Refl
||| Inhabitants of `Fin n` witness `NonZero n`
export
finNonZero : Fin n -> NonZero n
finNonZero FZ = SIsNonZero
finNonZero (FS i) = SIsNonZero
finNonZero FZ = ItIsSucc
finNonZero (FS i) = ItIsSucc

||| Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty
export
finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs
finNonEmpty xs SIsNonZero = replace {p = NonEmpty} (etaCons xs) IsNonEmpty
finNonEmpty xs ItIsSucc = replace {p = NonEmpty} (etaCons xs) IsNonEmpty

||| Cast an index into a runtime-irrelevant `Vect` into the position
||| of the corresponding element
Expand Down
2 changes: 1 addition & 1 deletion libs/papers/Search/Auto.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ namespace RuleName
where
display : Nat -> List Char
display n =
let (p, q) = divmodNatNZ n 26 SIsNonZero in
let (p, q) = divmodNatNZ n 26 ItIsSucc in
cast (q + cast 'a') :: if p == 0 then [] else display (assert_smaller n (pred p))


Expand Down
Loading