sized-types-0.3.5.2: Sized types in Haskell.

Safe HaskellSafe
LanguageHaskell98

Data.Sized.Arith

Description

Basic type-level arithmetic, using base two.

Copyright: (c) 2009 University of Kansas License: BSD3

Maintainer: Andy Gill andygill@ku.edu Stability: unstable Portability: ghc

Documentation

data N1 Source #

Instances

type APP0 N1 Source # 
type APP0 N1 = X0_ N1
type APP1 N1 Source # 
type APP1 N1 = N1
type SUCC N1 Source # 
type SUCC N1 = X0
type NOT N1 Source # 
type NOT N1 = X0
type MUL x N1 Source # 
type MUL x N1 = SUB X0 x
type ADD X0 N1 Source # 
type ADD X0 N1 = N1
type ADD N1 N1 Source # 
type ADD N1 N1 = APP0 N1
type ADD N1 (X1_ b) Source # 
type ADD N1 (X1_ b) = APP0 b
type ADD N1 (X0_ b) Source # 
type ADD N1 (X0_ b) = APP1 (ADD N1 b)
type ADD (X1_ a) N1 Source # 
type ADD (X1_ a) N1 = APP0 a
type ADD (X0_ a) N1 Source # 
type ADD (X0_ a) N1 = APP1 (ADD a N1)

data X0 Source #

Constructors

X0 

Instances

Eq X0 Source # 

Methods

(==) :: X0 -> X0 -> Bool #

(/=) :: X0 -> X0 -> Bool #

Ord X0 Source # 

Methods

compare :: X0 -> X0 -> Ordering #

(<) :: X0 -> X0 -> Bool #

(<=) :: X0 -> X0 -> Bool #

(>) :: X0 -> X0 -> Bool #

(>=) :: X0 -> X0 -> Bool #

max :: X0 -> X0 -> X0 #

min :: X0 -> X0 -> X0 #

Size X0 Source # 
type APP0 X0 Source # 
type APP0 X0 = X0
type APP1 X0 Source # 
type APP1 X0 = X1_ X0
type LOG X0 Source # 
type LOG X0 = X0
type SUCC X0 Source # 
type SUCC X0 = X1_ X0
type NOT X0 Source # 
type NOT X0 = N1
type Index X0 Source # 
type Index X0 = Int
type MUL x X0 Source # 
type MUL x X0 = X0
type ADD a X0 Source # 
type ADD a X0 = a
type ADD X0 a Source # 
type ADD X0 a = a
type ADD X0 N1 Source # 
type ADD X0 N1 = N1

data X0_ a Source #

Constructors

X0_ Integer 

Instances

Size a => Size (X0_ a) Source # 

Methods

size :: X0_ a -> Int Source #

addIndex :: X0_ a -> Index (X0_ a) -> X0_ a Source #

toIndex :: X0_ a -> Index (X0_ a) Source #

type MUL x (X0_ b) Source # 
type MUL x (X0_ b) = ADD x (MUL x (ADD (X0_ b) N1))
type ADD N1 (X0_ b) Source # 
type ADD N1 (X0_ b) = APP1 (ADD N1 b)
type APP0 (X0_ a) Source # 
type APP0 (X0_ a) = X0_ (X0_ a)
type APP1 (X0_ a) Source # 
type APP1 (X0_ a) = X1_ (X0_ a)
type LOG (X0_ a) Source # 
type LOG (X0_ a) = ADD (X1_ X0) (LOG a)
type SUCC (X0_ a) Source # 
type SUCC (X0_ a) = APP1 a
type NOT (X0_ a) Source # 
type NOT (X0_ a) = APP1 (NOT a)
type Index (X0_ a) Source # 
type Index (X0_ a) = Int
type ADD (X0_ a) N1 Source # 
type ADD (X0_ a) N1 = APP1 (ADD a N1)
type ADD (X1_ a) (X0_ b) Source # 
type ADD (X1_ a) (X0_ b) = APP1 (ADD a b)
type ADD (X0_ a) (X1_ b) Source # 
type ADD (X0_ a) (X1_ b) = APP1 (ADD a b)
type ADD (X0_ a) (X0_ b) Source # 
type ADD (X0_ a) (X0_ b) = APP0 (ADD a b)

data X1_ a Source #

Constructors

X1_ Integer 

Instances

Size a => Size (X1_ a) Source # 

Methods

size :: X1_ a -> Int Source #

addIndex :: X1_ a -> Index (X1_ a) -> X1_ a Source #

toIndex :: X1_ a -> Index (X1_ a) Source #

type MUL x (X1_ b) Source # 
type MUL x (X1_ b) = ADD x (MUL x (ADD (X1_ b) N1))
type ADD N1 (X1_ b) Source # 
type ADD N1 (X1_ b) = APP0 b
type APP0 (X1_ a) Source # 
type APP0 (X1_ a) = X0_ (X1_ a)
type APP1 (X1_ a) Source # 
type APP1 (X1_ a) = X1_ (X1_ a)
type LOG (X1_ a) Source # 
type LOG (X1_ a) = ADD (X1_ X0) (LOG a)
type SUCC (X1_ a) Source # 
type SUCC (X1_ a) = APP0 (SUCC a)
type NOT (X1_ a) Source # 
type NOT (X1_ a) = APP0 (NOT a)
type Index (X1_ a) Source # 
type Index (X1_ a) = Int
type ADD (X1_ a) N1 Source # 
type ADD (X1_ a) N1 = APP0 a
type ADD (X1_ a) (X0_ b) Source # 
type ADD (X1_ a) (X0_ b) = APP1 (ADD a b)
type ADD (X1_ a) (X1_ b) Source # 
type ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b))
type ADD (X0_ a) (X1_ b) Source # 
type ADD (X0_ a) (X1_ b) = APP1 (ADD a b)

type family ADD a b Source #

Instances

type ADD a X0 Source # 
type ADD a X0 = a
type ADD X0 a Source # 
type ADD X0 a = a
type ADD X0 N1 Source # 
type ADD X0 N1 = N1
type ADD N1 N1 Source # 
type ADD N1 N1 = APP0 N1
type ADD N1 (X1_ b) Source # 
type ADD N1 (X1_ b) = APP0 b
type ADD N1 (X0_ b) Source # 
type ADD N1 (X0_ b) = APP1 (ADD N1 b)
type ADD (X1_ a) N1 Source # 
type ADD (X1_ a) N1 = APP0 a
type ADD (X0_ a) N1 Source # 
type ADD (X0_ a) N1 = APP1 (ADD a N1)
type ADD (X1_ a) (X0_ b) Source # 
type ADD (X1_ a) (X0_ b) = APP1 (ADD a b)
type ADD (X1_ a) (X1_ b) Source # 
type ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b))
type ADD (X0_ a) (X1_ b) Source # 
type ADD (X0_ a) (X1_ b) = APP1 (ADD a b)
type ADD (X0_ a) (X0_ b) Source # 
type ADD (X0_ a) (X0_ b) = APP0 (ADD a b)

type family NOT a Source #

Instances

type NOT X0 Source # 
type NOT X0 = N1
type NOT N1 Source # 
type NOT N1 = X0
type NOT (X1_ a) Source # 
type NOT (X1_ a) = APP0 (NOT a)
type NOT (X0_ a) Source # 
type NOT (X0_ a) = APP1 (NOT a)

type SUB a b = ADD a (SUCC (NOT b)) Source #

type family MUL a b Source #

Instances

type MUL x X0 Source # 
type MUL x X0 = X0
type MUL x N1 Source # 
type MUL x N1 = SUB X0 x
type MUL x (X1_ b) Source # 
type MUL x (X1_ b) = ADD x (MUL x (ADD (X1_ b) N1))
type MUL x (X0_ b) Source # 
type MUL x (X0_ b) = ADD x (MUL x (ADD (X0_ b) N1))

type family SUCC a Source #

Instances

type SUCC X0 Source # 
type SUCC X0 = X1_ X0
type SUCC N1 Source # 
type SUCC N1 = X0
type SUCC (X1_ a) Source # 
type SUCC (X1_ a) = APP0 (SUCC a)
type SUCC (X0_ a) Source # 
type SUCC (X0_ a) = APP1 a

type family LOG a Source #

Instances

type LOG X0 Source # 
type LOG X0 = X0
type LOG (X1_ a) Source # 
type LOG (X1_ a) = ADD (X1_ X0) (LOG a)
type LOG (X0_ a) Source # 
type LOG (X0_ a) = ADD (X1_ X0) (LOG a)

type family APP1 a Source #

Instances

type APP1 X0 Source # 
type APP1 X0 = X1_ X0
type APP1 N1 Source # 
type APP1 N1 = N1
type APP1 (X1_ a) Source # 
type APP1 (X1_ a) = X1_ (X1_ a)
type APP1 (X0_ a) Source # 
type APP1 (X0_ a) = X1_ (X0_ a)

type family APP0 a Source #

Instances

type APP0 X0 Source # 
type APP0 X0 = X0
type APP0 N1 Source # 
type APP0 N1 = X0_ N1
type APP0 (X1_ a) Source # 
type APP0 (X1_ a) = X0_ (X1_ a)
type APP0 (X0_ a) Source # 
type APP0 (X0_ a) = X0_ (X0_ a)