--
-- 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 Integer type
--

-- 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

show_Integer : Show Integer
show_Integer = rec show = prim_show_Int



-- 
-- The String type
--

-- Instances:

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


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

show_String : Show String
show_String = rec show = prim_show_Str


--
-- The Bool type
--

data Bool : Type where 
	True : Bool
	False : Bool

-- derive Show Bool
-- derive Eq Bool
-- derive Ord Bool

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

-- Instances:

neg_Bool : Neg Bool
neg_Bool = rec negate = not

add_Bool : Add Bool
add_Bool = rec zero = False
               plus = \x -> \y -> x || y

mul_Bool : Add Bool
mul_Bool = rec one = True
               times = \x -> \y -> x && y




--
-- The List type
--

data List : (_:Type) -> Type where 
	Nil : (A:Type) -> List A
        Cons : (A:Type) -> A -> List A -> List A

size : (A:Type) -> List A -> Nat
size _ (Nil _) = Zero
size A (Cons _ x xs) = Succ (size A xs)

map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
map _ B _ (Nil _) = Nil B
map A B f (Cons _ x xs) = Cons B (f x) (map A B f xs)

append : (A:Type) -> List A -> List A -> List A
append A xs ys = foldr A (List A) (Cons A) ys xs

concat : (A : Type) -> List (List A) -> List A
concat A = foldr (List A) (List A) (append A) (Nil A)

foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B
foldr _ _ _ x (Nil _) = x
foldr A B f x (Cons _ y ys) = f y (foldr A B f x ys)

-- Instances:

add_List : (A : Type) -> Add (List A)
add_List A = rec zero = Nil A
		 plus = append A


monad_List : Monad List
monad_list = rec return = \A -> \x -> Cons A x (Nil A)
		 bind = \A -> \B -> \m -> \k -> concat B (map A B k m)





--
-- The Maybe type
--

data Maybe : Type -> Type where
	Nothing : (A : Type) -> Maybe A
	Just : (A : Type) -> A -> Maybe A

-- derive Show Maybe
-- derive Eq Maybe
-- derive Ord Maybe


fromMaybe : (A : Type) -> A -> Maybe A -> A
fromMaybe _ x Nothing = x
fromMaybe _ _ (Just x) = x

maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A
maybe _ _ x _ Nothing = x
maybe _ _ _ f (Just x) = f x


-- Instances:

monad_Maybe : Monad Maybe
monad_Maybe = 
  rec return = Just
      bind = \A -> \B -> \m -> \k -> 
         case m of
		Nothing _ -> Nothing B
		Just _ x  -> k x




--
-- 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




--
-- 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 A d = foldr A A d.plus d.zero


-- Operators:

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





--
-- The Sub class
--

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

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





--
-- 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 A d = foldr A A d.times d.one

-- Operators:

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




--
-- 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)
-}





--
-- 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
-}




--
-- 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)
-}





--
-- 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)
-}






--
-- The Show class
--

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

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






--
-- The Monoid class
--

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




--
-- The Compos class
--

Compos : (C : Type) -> (C -> Type) -> Type
Compos C T = sig 
  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 : (C : Type) -> (T : C -> Type) -> (d : Compos C T) 
        -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c
composOp _ _ d = d.composOp

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





--
-- The Monad class
--

Monad : (Type -> Type) -> Type
Monad M = sig return : (A : Type) -> M A
	      bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B

return : (M : Type -> Type) -> Monad M -> M A
return _ d = d.return

bind : (M : Type -> Type) -> Monad M 
    -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B
bind _ d = d.bind

-- Operators:

{-
  (x >>= y) => bind ? ? ? ? x y
  (x >>  y) => bind ? ? ? ? x (\_ -> y)
-}