sized-types-0.3.5.1: Sized types in Haskell.

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 = X0_ N1 type APP1 N1 = N1 type SUCC N1 = X0 type NOT N1 = X0 type MUL x N1 = SUB X0 x type ADD X0 N1 = N1 type ADD N1 N1 = APP0 N1 type ADD N1 (X1_ b) = APP0 b type ADD N1 (X0_ b) = APP1 (ADD N1 b) type ADD (X1_ a) N1 = APP0 a type ADD (X0_ a) N1 = APP1 (ADD a N1)

data X0 Source

Constructors

 X0

Instances

 Bounded X0 Enum X0 Eq X0 Integral X0 Num X0 Ord X0 Real X0 Show X0 Ix X0 Size X0 type APP0 X0 = X0 type APP1 X0 = X1_ X0 type LOG X0 = X0 type SUCC X0 = X1_ X0 type NOT X0 = N1 type Index X0 = Int type MUL x X0 = X0 type ADD a X0 = a type ADD X0 a = a type ADD X0 N1 = N1

data X0_ a Source

Constructors

 X0_ Integer

Instances

 Size a => Bounded (X0_ a) Size a => Enum (X0_ a) Eq (X0_ a) (Size a, Size (X0_ a), Integral a) => Integral (X0_ a) Size a => Num (X0_ a) Ord (X0_ a) Size a => Real (X0_ a) Show (X0_ a) Size a => Ix (X0_ a) Size a => Size (X0_ a) type MUL x (X0_ b) = ADD x (MUL x (ADD (X0_ b) N1)) type ADD N1 (X0_ b) = APP1 (ADD N1 b) type APP0 (X0_ a) = X0_ (X0_ a) type APP1 (X0_ a) = X1_ (X0_ a) type LOG (X0_ a) = ADD (X1_ X0) (LOG a) type SUCC (X0_ a) = APP1 a type NOT (X0_ a) = APP1 (NOT a) type Index (X0_ a) = Int type ADD (X0_ a) N1 = APP1 (ADD a N1) type ADD (X1_ a) (X0_ b) = APP1 (ADD a b) type ADD (X0_ a) (X1_ b) = APP1 (ADD a b) type ADD (X0_ a) (X0_ b) = APP0 (ADD a b)

data X1_ a Source

Constructors

 X1_ Integer

Instances

 Size a => Bounded (X1_ a) Size a => Enum (X1_ a) Eq (X1_ a) (Size a, Size (X1_ a), Integral a) => Integral (X1_ a) Size a => Num (X1_ a) Ord (X1_ a) Size a => Real (X1_ a) Show (X1_ a) Size a => Ix (X1_ a) Size a => Size (X1_ a) type MUL x (X1_ b) = ADD x (MUL x (ADD (X1_ b) N1)) type ADD N1 (X1_ b) = APP0 b type APP0 (X1_ a) = X0_ (X1_ a) type APP1 (X1_ a) = X1_ (X1_ a) type LOG (X1_ a) = ADD (X1_ X0) (LOG a) type SUCC (X1_ a) = APP0 (SUCC a) type NOT (X1_ a) = APP0 (NOT a) type Index (X1_ a) = Int type ADD (X1_ a) N1 = APP0 a type ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b)) type ADD (X1_ a) (X0_ b) = APP1 (ADD a b) type ADD (X0_ a) (X1_ b) = APP1 (ADD a b)

type family ADD a b Source

Instances

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

type family NOT a Source

Instances

 type NOT X0 = N1 type NOT N1 = X0 type NOT (X1_ a) = APP0 (NOT a) 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 N1 = SUB X0 x type MUL x X0 = X0 type MUL x (X1_ b) = ADD x (MUL x (ADD (X1_ b) N1)) type MUL x (X0_ b) = ADD x (MUL x (ADD (X0_ b) N1))

type family SUCC a Source

Instances

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

type family LOG a Source

Instances

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

type family APP1 a Source

Instances

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

type family APP0 a Source

Instances

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