path: root/transfer/lib/prelude.tr

--
-- Prelude for the transfer language.
--


--
-- Basic functions
--

const : (A:Type) -> (B:Type) -> A -> B -> A
const _ _ x _ = x

id : (A:Type) -> A -> A
id _ x = x


--
-- The Bool type
--

data Bool : Type where 
	True : Bool
	False : Bool

not : Bool -> Bool
not b = if b then False else True


--
-- The Num class
--

Num : Type -> Type
Num = sig zero : A
	  plus : A -> A -> A
	  minus : A -> A -> A
	  one : A
	  times : A -> A -> A
	  div : A -> A -> A
	  mod : A -> A -> A
	  negate : A -> A
	  eq : A -> A -> Bool
	  compare : A -> A -> Ordering

-- Instances:

num_Integer : Num Integer
num_Integer = rec zero = 0
		  plus = prim_add_Int
		  minus = prim_sub_Int
		  one = 1
              	  times = prim_mul_Int
		  div = prim_div_Int
              	  mod = prim_mod_Int
		  negate = prim_neg_Int
		  eq = prim_eq_Int
		  compare = prim_cmp_Int

--
-- The Add class
--

Add : Type -> Type
Add = sig zero : A
	  plus : A -> A -> A

zero : (A : Type) -> Add A -> A
zero _ d = d.zero

plus : (A : Type) -> Add A -> A -> A -> A
plus _ d = d.plus

sum : (A:Type) -> Add A -> List A -> A
sum _ d (Nil _) = d.zero
sum A d (Cons _ x xs) = d.plus x (sum A d xs)

-- Operators:

{-
  (x + y) => (plus ? ? x y)
-}

-- Instances:

-- num_Integer

add_String : Add String
add_String = rec zero = ""
		 plus = prim_add_Str

--
-- The Sub class
--

Sub : Type -> Type
Sub = sig minus : A -> A -> A

minus : (A : Type) -> Sub A -> A
minus _ d = d.minus

-- Instances:

-- num_Integer


--
-- The Mul class
--

Mul : Type -> Type
Mul = sig one : A
	  times : A -> A -> A

one : (A : Type) -> Mul A -> A
one _ d = d.one

times : (A : Type) -> Mul A -> A -> A -> A
times _ d = d.times

product : (A:Type) -> Mul A -> List A -> A
product _ d (Nil _) = d.one
product A d (Cons _ x xs) = d.times x (product A d xs)

-- Operators:

{- 
  (x * y) => (times ? ? x y)
-}

-- Instances:

-- num_Integer


--
-- The Div class
--

Div : Type -> Type
Div = sig div : A -> A -> A
	  mod : A -> A -> A

div : (A : Type) -> Div A -> A -> A -> A
div _ d = d.div

mod : (A : Type) -> Div A -> A -> A -> A
mod _ d = d.mod

-- Operators:

{- 
  (x / y) => (div ? ? x y)
  (x % y) => (mod ? ? x y)
-}

-- Instances:

-- num_Integer



--
-- The Neg class
--

Neg : Type -> Type
Neg = sig negate : A -> A

negate : (A : Type) -> Neg A -> A -> A
negate _ d = d.neg

-- Operators:

{-
  (-x) => negate ? ? x
-}

-- Instances:

-- num_Integer

neg_Bool : Neg Bool
neg_Bool = rec negate = not



--
-- The Eq class
--

Eq : Type -> Type
Eq A = sig eq : A -> A -> Bool

eq : (A : Type) -> Eq A -> A -> A -> Bool
eq _ d = d.eq

neq : (A : Type) -> Eq A -> A -> A -> Bool
neq A d x y = not (eq A d x y)


-- Operators:

{-
  (x == y) => (eq ? ? x y)
  (x /= y) => (neq ? ? x y)
-}

-- Instances:

-- num_Integer

eq_String : Eq String
eq_String = rec eq = prim_eq_Str



--
-- The Ord class
--

data Ordering : Type where
	LT : Ordering
	EQ : Ordering
	GT : Ordering

Ord : Type -> Type
Ord A = sig eq : A -> A -> Bool
	    compare : A -> A -> Ordering

compare : (A : Type) -> Ord A -> A -> A -> Ordering
compare _ d = d.compare

ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool
ordOp f A d x y = f (compare A d x y)

lt : (A : Type) -> Ord A -> A -> A -> Bool
lt = ordOp (\o -> case o of { LT -> True; _ -> False })

le : (A : Type) -> Ord A -> A -> A -> Bool
le = ordOp (\o -> case o of { GT -> False; _ -> True })

ge : (A : Type) -> Ord A -> A -> A -> Bool
ge = ordOp (\o -> case o of { LT -> False; _ -> True })

gt : (A : Type) -> Ord A -> A -> A -> Bool
gt = ordOp (\o -> case o of { GT -> True; _ -> False })

-- Operators:

{- 
  (x < y) => (lt ? ? x y)
  (x <= y) => (le ? ? x y)
  (x >= y) => (ge ? ? x y)
  (x > y) => (gt ? ? x y)
-}

-- Instances:

-- num_Integer

ord_String : Ord String
ord_String = rec eq = prim_eq_Str
		 compare = prim_cmp_Str



--
-- The Show class
--

Show : Type -> Type
Show A = sig show : A -> String

show : (A : Type) -> Show A -> A -> String
show _ d = d.show


-- Instances:

show_Integer : Show Integer
show_Integer = rec show = prim_show_Int

show_String : Show String
show_String = rec show = prim_show_Str



--
-- The Monoid class
--

Monoid : Type -> Type
Monoid = sig mzero : A
	     mplus : A -> A -> A



--
-- The Compos class
--

Compos : Type -> Type
Compos T = sig 
  C : Type
  composOp : (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c
  composFold : (B : Type) -> Monoid B -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b

composOp : (T : Type) -> (d : Compos T) 
        -> (c : d.C) -> ((a : d.C) -> T a -> T a) -> T c -> T c
composOp _ d = d.composOp

composFold : (T : Type) -> (d : Compos T) -> (B : Type) -> Monoid B 
          -> (c : d.C) -> ((a : d.C) -> T a -> b) -> T c -> b
composFold _ _ d = d.composFold