module Prelude import Builtins import IO import Prelude.Cast import Prelude.Nat import Prelude.Fin import Prelude.List import Prelude.Maybe import Prelude.Monad import Prelude.Applicative import Prelude.Either import Prelude.Vect import Prelude.Strings import Prelude.Chars %access public %default total -- Show and instances class Show a where show : a -> String instance Show Nat where show O = "O" show (S k) = "s" ++ show k instance Show Int where show = prim__intToStr instance Show Integer where show = prim__bigIntToStr instance Show Float where show = prim__floatToStr instance Show Char where show x = strCons x "" instance Show String where show = id instance Show Bool where show True = "True" show False = "False" instance (Show a, Show b) => Show (a, b) where show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")" instance Show a => Show (List a) where show xs = "[" ++ show' "" xs ++ "]" where show' : String -> List a -> String show' acc [] = acc show' acc [x] = acc ++ show x show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs instance Show a => Show (Vect a n) where show xs = "[" ++ show' xs ++ "]" where show' : Vect a m -> String show' [] = "" show' [x] = show x show' (x :: xs) = show x ++ ", " ++ show' xs instance Show a => Show (Maybe a) where show Nothing = "Nothing" show (Just x) = "Just " ++ show x ---- Monad instances instance Monad IO where return t = io_return t b >>= k = io_bind b k instance Monad Maybe where return t = Just t Nothing >>= k = Nothing (Just x) >>= k = k x instance MonadPlus Maybe where mzero = Nothing mplus (Just x) _ = Just x mplus Nothing (Just y) = Just y mplus Nothing Nothing = Nothing instance Monad List where return x = [x] m >>= f = concatMap f m instance MonadPlus List where mzero = [] mplus = (++) ---- Functor instances instance Functor Maybe where fmap f (Just x) = Just (f x) fmap f Nothing = Nothing instance Functor List where fmap = map ---- Applicative instances instance Applicative Maybe where pure = Just (Just f) <$> (Just a) = Just (f a) _ <$> _ = Nothing ---- some mathematical operations %include "math.h" %lib "m" exp : Float -> Float exp x = prim__floatExp x log : Float -> Float log x = prim__floatLog x pi : Float pi = 3.141592653589793 sin : Float -> Float sin x = prim__floatSin x cos : Float -> Float cos x = prim__floatCos x tan : Float -> Float tan x = prim__floatTan x asin : Float -> Float asin x = prim__floatASin x acos : Float -> Float acos x = prim__floatACos x atan : Float -> Float atan x = prim__floatATan x atan2 : Float -> Float -> Float atan2 y x = atan (y/x) sqrt : Float -> Float sqrt x = prim__floatSqrt x floor : Float -> Float floor x = prim__floatFloor x ceiling : Float -> Float ceiling x = prim__floatCeil x ---- Ranges partial count : (Ord a, Num a) => a -> a -> a -> List a count a inc b = if a <= b then a :: count (a + inc) inc b else [] partial countFrom : (Ord a, Num a) => a -> a -> List a countFrom a inc = a :: lazy (countFrom (a + inc) inc) syntax "[" [start] ".." [end] "]" = count start 1 end syntax "[" [start] "," [next] ".." [end] "]" = count start (next - start) end syntax "[" [start] "..]" = countFrom start 1 syntax "[" [start] "," [next] "..]" = countFrom start (next - start) ---- More utilities sum : Num a => List a -> a sum = foldl (+) 0 prod : Num a => List a -> a prod = foldl (*) 1 ---- some basic io partial putStr : String -> IO () putStr x = mkForeign (FFun "putStr" [FString] FUnit) x partial putStrLn : String -> IO () putStrLn x = putStr (x ++ "\n") partial print : Show a => a -> IO () print x = putStrLn (show x) partial getLine : IO String getLine = return (prim__readString prim__stdin) partial putChar : Char -> IO () putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c partial getChar : IO Char getChar = mkForeign (FFun "getchar" [] FChar) ---- some basic file handling abstract data File = FHandle Ptr do_fopen : String -> String -> IO Ptr do_fopen f m = mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m fopen : String -> String -> IO File fopen f m = do h <- do_fopen f m return (FHandle h) data Mode = Read | Write | ReadWrite partial openFile : String -> Mode -> IO File openFile f m = fopen f (modeStr m) where modeStr : Mode -> String modeStr Read = "r" modeStr Write = "w" modeStr ReadWrite = "r+" partial do_fclose : Ptr -> IO () do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h partial closeFile : File -> IO () closeFile (FHandle h) = do_fclose h partial do_fread : Ptr -> IO String do_fread h = return (prim__readString h) partial fread : File -> IO String fread (FHandle h) = do_fread h partial do_fwrite : Ptr -> String -> IO () do_fwrite h s = mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s partial fwrite : File -> String -> IO () fwrite (FHandle h) s = do_fwrite h s partial do_feof : Ptr -> IO Int do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h feof : File -> IO Bool feof (FHandle h) = do eof <- do_feof h return (not (eof == 0)) partial nullPtr : Ptr -> IO Bool nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p return (ok /= 0); partial validFile : File -> IO Bool validFile (FHandle h) = do x <- nullPtr h return (not x) partial -- obviously while : |(test : IO Bool) -> |(body : IO ()) -> IO () while t b = do v <- t if v then do b while t b else return () partial -- no error checking! readFile : String -> IO String readFile fn = do h <- openFile fn Read c <- readFile' h "" closeFile h return c where partial readFile' : File -> String -> IO String readFile' h contents = do x <- feof h if not x then do l <- fread h readFile' h (contents ++ l) else return contents