, Control.Show

import Control.Show

public export
Show Integer where
  show = prim__cast_IntegerString
%integerLit fromPrimInteger
public export
interface SupportPrimIntegerLiteral t where
  PrimIntegerRestriction : Integer -> Type
  fromPrimInteger : (x : Integer) -> {auto ok : PrimIntegerRestriction x} -> t
  toPrimInteger : t -> Integer
public export
SupportPrimIntegerLiteral Integer where
  PrimIntegerRestriction x = Unit
  fromPrimInteger x = x
  toPrimInteger = identity

import Data.PrimInteger

import public Control.Show
import public Data.PrimInteger

natFromPrimInteger : (x : Integer) -> {auto ok : x `GTE` 0} -> Natural
natFromPrimInteger 0 = Zero
natFromPrimInteger x = case (decGTE (prim__sub_Integer x 1) 0) of
  Yes p => Succesor $ assert_total $ natFromPrimInteger $ prim__sub_Integer x 1
  No cp => void $ believe_me () -- TODO: impossible
%builtin IntegerToNatural natFromPrimInteger
natToPrimInteger : Natural -> Integer
natToPrimInteger Zero = 0
natToPrimInteger (Succesor x) = prim__add_Integer 1 $ natToPrimInteger x

%builtin NaturalToInteger natToPrimInteger

fromInteger : (x : Integer) -> {auto ok : x `GTE` 0} -> Natural
fromInteger 0 = Zero
fromInteger x = case (decGTE (prim__sub_Integer x 1) 0) of
  Yes p => Succesor $ assert_total $ fromInteger $ prim__sub_Integer x 1
  No cp => void $ believe_me ()

SupportPrimIntegerLiteral Natural where
  PrimIntegerRestriction x = x `GTE` 0
  fromPrimInteger = natFromPrimInteger
  toPrimInteger   = natToPrimInteger

%integerLit fromInteger

public export
Show Natural where
  show = show . toPrimInteger

module Control.Show
public export
interface Show t where
  show : t -> String