
  0 | module Data.IntegralGCD
  1 | 
  2 | %default total
  3 | 
  4 | 
  5 | ||| An interface for integer types that it is possible to take the GCD
  6 | ||| (greatest common denominator) of.
  7 | |||
  8 | ||| This interface exists for totality purposes: Euclid's algorithm is
  9 | ||| possible to implement for any type that satisfies `Integral`, but it
 10 | ||| is not provably total unless that implementation satisfies some properties.
 11 | |||
 12 | ||| Implementing this interface asserts to the compiler that Euclid's algorithm
 13 | ||| is total on this type.
 14 | public export
 15 | interface (Eq a, Integral a) => IntegralGCD a where
 16 |   gcd : a -> a -> a
 17 |   gcd x y =
 18 |     if x == 0 then y
 19 |     else if y == 0 then x
 20 |     else gcd y (assert_smaller y $ x `mod` y)
 21 | 
 22 | 
 23 | export IntegralGCD Integer where
 24 | 
 25 | export IntegralGCD Int where
 26 | export IntegralGCD Int8 where
 27 | export IntegralGCD Int16 where
 28 | export IntegralGCD Int32 where
 29 | export IntegralGCD Int64 where
 30 | 
 31 | export IntegralGCD Bits8 where
 32 | export IntegralGCD Bits16 where
 33 | export IntegralGCD Bits32 where
 34 | export IntegralGCD Bits64 where
 35 |