Transfer: Changed transfer program file extension from .tr to .tra to avoid collision with Troff file extension.

transfer/lib/prelude.tra

@@ -0,0 +1,502 @@
+--
+-- 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
+
+flip : (A:Type) -> (B:Type) -> (C:Type) -> (A -> B -> C) -> B -> A -> C
+flip _ _ _ f x y = f y x
+
+compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C
+compose _ _ _ f g x = f (g x)
+
+otherwise : Bool
+otherwise = True
+
+
+--
+-- The Integer type
+--
+
+-- Instances:
+
+num_Integer : Num Integer
+num_Integer = rec zero = 0
+		  plus = prim_add_Integer
+		  minus = prim_sub_Integer
+		  one = 1
+              	  times = prim_mul_Integer
+		  div = prim_div_Integer
+              	  mod = prim_mod_Integer
+		  negate = prim_neg_Integer
+		  eq = prim_eq_Integer
+		  compare = prim_cmp_Integer
+
+show_Integer : Show Integer
+show_Integer = rec show = prim_show_Integer
+
+
+--
+-- The Double type
+--
+
+-- Instances:
+
+num_Double : Num Double
+num_Double = rec zero = 0.0
+		 plus = prim_add_Double
+		 minus = prim_sub_Double
+		 one = 1.0
+              	 times = prim_mul_Double
+		 div = prim_div_Double
+              	 mod = prim_mod_Double
+		 negate = prim_neg_Double
+		 eq = prim_eq_Double
+		 compare = prim_cmp_Double
+
+show_Double : Show Double
+show_Double = rec show = prim_show_Double
+
+
+
+-- 
+-- The String type
+--
+
+-- Instances:
+
+add_String : Add String
+add_String = rec zero = ""
+		 plus = prim_add_String
+
+
+ord_String : Ord String
+ord_String = rec eq = prim_eq_Str
+		 compare = prim_cmp_String
+
+show_String : Show String
+show_String = rec show = prim_show_String
+
+
+--
+-- 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
+
+
+--
+-- Tuples
+--
+
+Pair : Type -> Type -> Type
+Pair A B = sig { p1 : A; p2 : B }
+
+pair : (A:Type) -> (B:Type) -> A -> B -> Pair A B
+pair _ _ x y = rec { p1 = x; p2 = y }
+
+fst : (A:Type) -> (B:Type) -> Pair A B -> A
+fst _ _ p = case p of Pair _ _ x _ -> x
+
+snd : (A:Type) -> (B:Type) -> Pair A B -> B
+snd _ _ p = case p of Pair _ _ x _ -> x
+
+{-
+
+ syntax:
+
+ (x1,...,xn) => { p1 = e1; ... ; pn = en }
+
+ where n >= 2 and x1,...,xn are expressions or patterns
+
+-}
+
+
+--
+-- The List type
+--
+
+data List : Type -> Type where 
+	Nil : (A:Type) -> List A
+        Cons : (A:Type) -> A -> List A -> List A
+
+foldr : (A : Type) -> (B : Type) -> (A -> B -> B) -> B -> List A -> B
+foldr _ _ _ x [] = x
+foldr A B f x (y::ys) = f y (foldr A B f x ys)
+
+length : (A:Type) -> List A -> Integer
+length A = foldr A Integer (\_ -> \y -> y+1) 0
+
+map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
+map _ _ _ [] = []
+map A B f (x::xs) = f x :: map A B f xs
+
+filter : (A:Type) -> (A -> Bool) -> List A -> List A
+filter _ _ []            = []
+filter A f (x::xs) | f x = x :: filter A f xs
+filter A f (x::xs)       = filter A 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)
+
+partition : (A : Type) -> (A -> Bool) -> List A -> Pair (List A) (List A)
+partition _ _ [] = ([],[])
+partition A p (x::xs) = 
+  let r : Pair (List A) (List A) = partition A p xs
+   in if p x then (x :: fst r, snd r) else (fst r, x :: snd r)
+
+
+-- 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.negate
+
+-- 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)
+-}
+