0 | module Data.Nat1
  1 |
  2 | import public Data.Nat
  3 | import public Data.DPair
  4 | import Data.CheckedEmpty.List.Lazy
  5 | import public Data.So
  6 |
  7 | %default total
  8 |
  9 | --- Type definition ---
 10 |
 11 | public export
 12 | data Nat1 : Type where
 13 |   FromNat : (n : Nat) -> (0 _ : IsSucc n) => Nat1
 14 |
 15 | --- Covertions ---
 16 |
 17 | public export
 18 | toNat1 : Nat -> Maybe Nat1
 19 | toNat1 Z       = Nothing
 20 | toNat1 k@(S _) = Just $ FromNat k
 21 |
 22 | public export %inline
 23 | fromNat : (x : Nat) -> (0 _ : IsSucc x) => Nat1
 24 | fromNat = FromNat
 25 |
 26 | public export %inline
 27 | toNat, (.asNat) : Nat1 -> Nat
 28 | toNat $ FromNat n = n
 29 | (.asNat) = toNat
 30 |
 31 | --- Implementations of basic interfaces ---
 32 |
 33 | public export
 34 | Eq Nat1 where
 35 |   FromNat n == FromNat n' = n == n'
 36 |
 37 | public export
 38 | Ord Nat1 where
 39 |   compare = comparing $ \(FromNat n) => n
 40 |
 41 | --- Literals syntax support ---
 42 |
 43 | public export %inline
 44 | fromInteger : (x : Integer) -> (0 _ : So $ x >= 1) => Nat1
 45 | fromInteger x = FromNat (cast x) @{believe_me $ ItIsSucc {n=1}}
 46 |
 47 | export
 48 | Range Nat1 where
 49 |   rangeFrom fr = rangeFrom fr.asNat <&> \x => FromNat x @{believe_me $ ItIsSucc {n=1}}
 50 |   rangeFromThen fr th = rangeFromThen fr.asNat th.asNat <&> \x => FromNat x @{believe_me $ ItIsSucc {n=1}}
 51 |   rangeFromTo fr to = rangeFromTo fr.asNat to.asNat <&> \x => FromNat x @{believe_me $ ItIsSucc {n=1}}
 52 |   rangeFromThenTo fr th to = rangeFromThenTo fr.asNat th.asNat to.asNat <&> \x => FromNat x @{believe_me $ ItIsSucc {n=1}}
 53 |
 54 | --- Simple arithmetics ---
 55 |
 56 | public export %inline
 57 | succ : Nat1 -> Nat1
 58 | succ $ FromNat n = FromNat (S n)
 59 |
 60 | public export %inline
 61 | one : Nat1
 62 | one = 1
 63 |
 64 | public export %inline
 65 | (+) : Nat1 -> Nat1 -> Nat1
 66 | FromNat (S n) + FromNat (S m) = FromNat (S n + S m)
 67 |
 68 | public export %inline
 69 | (*) : Nat1 -> Nat1 -> Nat1
 70 | FromNat (S n) * FromNat (S m) = FromNat (S n * S m)
 71 |
 72 | --- Semigroups and etc ---
 73 |
 74 | namespace Semigroup
 75 |
 76 |   public export
 77 |   [Additive] Semigroup Nat1 where
 78 |     (<+>) = (+)
 79 |
 80 |   public export
 81 |   [Multiplicative] Semigroup Nat1 where
 82 |     (<+>) = (*)
 83 |
 84 | namespace Monoid
 85 |
 86 |   public export
 87 |   [Multiplicative] Monoid Nat1 using Nat1.Semigroup.Multiplicative where
 88 |     neutral = 1
 89 |
 90 |   public export
 91 |   [Maximum] Monoid Nat1 using Semigroup.Maximum where
 92 |     neutral = 1
 93 |
 94 | --- Greatest common divisor ---
 95 |
 96 | export
 97 | gcd : (a, b : Nat) -> (0 ok : Either (IsSucc a) (IsSucc b)) => Nat1
 98 | gcd Z Z       = void $ absurd ok
 99 | gcd a@(S _) Z = FromNat a
100 | gcd Z b@(S _) = FromNat b
101 | gcd a (S b)   = assert_total $ gcd (S b) (modNatNZ a (S b) %search)
102 |
103 | export
104 | gcd' : Nat1 -> Nat1 -> Nat1
105 | gcd' (FromNat n) (FromNat m) = gcd n m
106 |
107 | --- Working with weighted lists ---
108 |
109 | -- TODO to make this to be dependent on some interface for lazy folding of non-empty collections
110 | export
111 | pickWeighted : LazyLst1 (Nat1, a) -> Nat -> a
112 | pickWeighted [(_, x)]                     _ = x
113 | pickWeighted wh@((FromNat n, x)::y::ys) k = if k < n then x else pickWeighted (assert_smaller wh $ y::ys) (k `minus` n)
114 |
115 | foldmne : Foldable f => (a -> a -> a) -> f a -> Maybe a
116 | foldmne g = foldl gg Nothing where
117 |   gg : Maybe a -> a -> Maybe a
118 |   gg ml r = (ml <&> \l => g l r) <|> Just r
119 |
120 | export
121 | normaliseWeights : Foldable f => Functor f => f (Nat1, a) -> f (Nat1, a)
122 | normaliseWeights xs = do
123 |   let Just $ FromNat (S d) = foldmne gcd' $ Builtin.fst <$> xs
124 |     | Nothing => xs
125 |   flip map xs $ mapFst $ \(FromNat n) => FromNat (divNatNZ n (S d) %search) @{believe_me $ ItIsSucc {n=1} {- since divisor is GCD -}}
126 |