122 lines
3 KiB
Idris
122 lines
3 KiB
Idris
module Quox.NatExtra
|
|
|
|
import public Data.Nat
|
|
import Data.Nat.Division
|
|
import Data.SnocList
|
|
import Data.Vect
|
|
import Data.String
|
|
import Quox.Decidable
|
|
|
|
%default total
|
|
|
|
|
|
public export
|
|
data LTE' : Nat -> Nat -> Type where
|
|
LTERefl : LTE' n n
|
|
LTESuccR : LTE' m n -> LTE' m (S n)
|
|
%builtin Natural LTE'
|
|
%name LTE' p, q
|
|
|
|
public export %hint
|
|
lteZero' : {n : Nat} -> LTE' 0 n
|
|
lteZero' {n = 0} = LTERefl
|
|
lteZero' {n = S n} = LTESuccR lteZero'
|
|
%transform "NatExtra.lteZero'" lteZero' {n} = believe_me n
|
|
|
|
public export %hint
|
|
lteSucc' : LTE' m n -> LTE' (S m) (S n)
|
|
lteSucc' LTERefl = LTERefl
|
|
lteSucc' (LTESuccR p) = LTESuccR $ lteSucc' p
|
|
%transform "NatExtra.lteSucc'" lteSucc' p = believe_me p
|
|
|
|
public export
|
|
fromLTE : {n : Nat} -> LTE m n -> LTE' m n
|
|
fromLTE LTEZero = lteZero'
|
|
fromLTE (LTESucc p) = lteSucc' $ fromLTE p
|
|
-- %transform "NatExtra.fromLTE"
|
|
-- fromLTE {n} p = believe_me (n `minus` believe_me p)
|
|
|
|
public export
|
|
toLTE : {m : Nat} -> m `LTE'` n -> m `LTE` n
|
|
toLTE LTERefl = reflexive
|
|
toLTE (LTESuccR p) = lteSuccRight (toLTE p)
|
|
-- %transform "NatExtra.toLTE" toLTE {m} p = believe_me m
|
|
|
|
public export
|
|
lteLTE' : {m, n : Nat} -> LTE m n <=> LTE' m n
|
|
lteLTE' = MkEquivalence fromLTE toLTE
|
|
|
|
public export
|
|
isLTE' : (m, n : Nat) -> Dec (LTE' m n)
|
|
isLTE' m n = map lteLTE' $ isLTE m n
|
|
|
|
|
|
public export
|
|
data LT' : Nat -> Nat -> Type where
|
|
LTZero : LT' 0 (S n)
|
|
LTSucc : LT' m n -> LT' (S m) (S n)
|
|
%builtin Natural LT'
|
|
%name LT' p, q
|
|
|
|
public export
|
|
Transitive Nat LT' where
|
|
transitive LTZero (LTSucc q) = LTZero
|
|
transitive (LTSucc p) (LTSucc q) = LTSucc $ transitive p q
|
|
|
|
|
|
private
|
|
0 baseNZ : n `GTE` 2 => NonZero n
|
|
baseNZ @{LTESucc _} = SIsNonZero
|
|
|
|
parameters {base : Nat} {auto 0 _ : base `GTE` 2} (chars : Vect base Char)
|
|
private
|
|
showAtBase' : List Char -> Nat -> List Char
|
|
showAtBase' acc 0 = acc
|
|
showAtBase' acc k =
|
|
let dig = natToFinLT (modNatNZ k base baseNZ) @{boundModNatNZ {}} in
|
|
showAtBase' (index dig chars :: acc)
|
|
(assert_smaller k $ divNatNZ k base baseNZ)
|
|
|
|
export
|
|
showAtBase : Nat -> String
|
|
showAtBase = pack . showAtBase' []
|
|
|
|
namespace Nat
|
|
export
|
|
showHex : Nat -> String
|
|
showHex = showAtBase $ fromList $ unpack "0123456789abcdef"
|
|
|
|
namespace Int
|
|
export
|
|
showHex : Int -> String
|
|
showHex x =
|
|
if x < 0 then "-" ++ Nat.showHex (cast (-x)) else Nat.showHex (cast x)
|
|
|
|
|
|
namespace Int
|
|
export
|
|
fromHexit : Char -> Maybe Int
|
|
fromHexit c =
|
|
if c >= '0' && c <= '9' then Just $ ord c - ord '0'
|
|
else if c >= 'a' && c <= 'f' then Just $ ord c - ord 'a' + 10
|
|
else if c >= 'A' && c <= 'F' then Just $ ord c - ord 'A' + 10
|
|
else Nothing
|
|
|
|
private
|
|
fromHex' : Int -> String -> Maybe Int
|
|
fromHex' acc str = case strM str of
|
|
StrNil => Just acc
|
|
StrCons c cs => fromHex' (16 * acc + !(fromHexit c)) (assert_smaller str cs)
|
|
|
|
export %inline
|
|
fromHex : String -> Maybe Int
|
|
fromHex str = do guard $ str /= ""; fromHex' 0 str
|
|
|
|
namespace Nat
|
|
export
|
|
fromHexit : Char -> Maybe Nat
|
|
fromHexit = map cast . Int.fromHexit
|
|
|
|
export %inline
|
|
fromHex : String -> Maybe Nat
|
|
fromHex = map cast . Int.fromHex
|