hmmm

drup.hs

{-# LANGUAGE GADTs,LambdaCase,RankNTypes #-}
-- Copyright SaladQL.com/licence
module Lib where
import Prelude hiding (succ, fromIntegral)
type Digit n = (Num n, Eq n, Show n) => n

data Nat where
  S     :: (Eq n, Eq z, Show n, Show z, Num n, Num z, n ~ z) => Digit z -> Digit n -> Nat
  Z     :: () -> Nat
  NZ    :: Nat -> Nat
  NS    :: (Digit n -> Digit n -> Nat) -> Nat -> Nat
  DIVzZ :: () ->  Nat

instance Num Nat where
instance Eq Nat where
  (Z _)    == (Z _)    = True
  (NZ z)   == (NZ n)   = z == n 
  (NS _ z) == (NS _ n) = z == n
  n == z               = False
  

-- showsPrec d x r ++ s  ==  showsPrec d x (r ++ s)
instance Show Nat where 
  showsPrec d (S z n)  = showsPrec d z . showsPrec d  '+' . showsPrec d n
  showsPrec d (Z _)    = showsPrec d (mempty :: String)
  showsPrec d (NZ z)   = showsPrec d '(' . showsPrec d z . showsPrec d ')'
  showsPrec d (NS _ m) = showsPrec d '(' . showsPrec d m . showsPrec d ')'
  showsPrec d (DIVzZ _)= showsPrec d "<<divding by zero already, son?>>"


(>>>) :: Nat -> Nat -> Nat
(>>>) z n = S z n

succ :: Nat -> Nat
succ btm@(DIVzZ _) = btm
succ f@(NZ _)      = NS (S) f
succ (NS _ o)      = NS (>>>) (shrink True o)


shrink :: Bool -> Nat -> Nat
shrink firstTime z@(Z _)
  | firstTime =  z
  | otherwise = DIVzZ ()

fromIntegralHelper :: forall n. (Show n, Num n, Eq n) => Digit n -> (Nat, n)
fromIntegralHelper = \n -> foldr (\_ (n,z) -> if z == 0 then (n,z) else (succ n,negate 1 + z)) (NZ(Z ()),n) (repeat ())
fromIntegral       :: forall n. (Show n, Num n, Eq n) =>  Digit n -> Nat
fromIntegral       = fst . fromIntegralHelper

data VDiv where
  VDiv :: Nat -> Nat -> Nat -> VDiv