Permalink
Browse files

More platform agnostic now

Cleaned up the paths, also added feof and ferror as functions (on
mingw32 they're macros that expand incorrectly in the C based backend
output.

Conflicts:
	src/Pkg/Package.hs
	src/Util/System.hs
  • Loading branch information...
1 parent 7fe382d commit fd5cddb529d9003a66fc6049e369de79c1fbe98c @chetant chetant committed with LeifWarner Nov 29, 2012
Showing with 399 additions and 405 deletions.
  1. +6 −3 Setup.hs
  2. +139 −139 contribs/lib/simpleparser.idr
  3. +1 −1 idris.cabal
  4. +10 −2 lib/Prelude.idr
  5. +155 −155 papers/impl-paper/impldtp.tex
  6. +10 −1 rts/idris_stdfgn.c
  7. +61 −61 src/Core/Constraints.hs
  8. +8 −14 src/Pkg/Package.hs
  9. +9 −29 src/Util/System.hs
View
@@ -7,7 +7,8 @@ import qualified Distribution.Simple.Program as P
import Distribution.PackageDescription
import System.Exit
-import System.FilePath ((</>))
+import System.FilePath ((</>), splitDirectories)
+import qualified System.FilePath.Posix as Px
import System.Process
-- After Idris is built, we need to check and install the prelude and other libs
@@ -16,9 +17,11 @@ make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "m
#ifdef mingw32_HOST_OS
-- make on mingw32 exepects unix style separators
-idrisCmd local = "../dist/build/idris/idris"
+(<//>) = (Px.</>)
+idrisCmd local = Px.joinPath $ splitDirectories $
+ ".." <//> buildDir local <//> "idris" <//> "idris"
#else
-idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
+idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"
#endif
cleanStdLib verbosity
@@ -1,153 +1,153 @@
-module Parsing
-
-import prelude
-import builtins
-
-infixr 5 |||
-
-{-
-The monad of parsers
---------------------
--}
-
-data Parser a = P (String -> Either String (a,String))
-
-parse : Parser a -> String ->Either String (a,String)
-parse (P p) inp = p inp
-
-instance Monad Parser where
- return v = P (\inp => Right (v,inp))
- p >>= f = P (\inp => case parse p inp of
- Left err => Left err
- Right (v,rest) => parse (f v) rest)
-
-
-instance MonadPlus Parser where
- mzero = P (\inp => Left "Parse Error")
- mplus p q = P (\inp => case parse p inp of
- Left msg => parse q inp
+module Parsing
+
+import prelude
+import builtins
+
+infixr 5 |||
+
+{-
+The monad of parsers
+--------------------
+-}
+
+data Parser a = P (String -> Either String (a,String))
+
+parse : Parser a -> String ->Either String (a,String)
+parse (P p) inp = p inp
+
+instance Monad Parser where
+ return v = P (\inp => Right (v,inp))
+ p >>= f = P (\inp => case parse p inp of
+ Left err => Left err
+ Right (v,rest) => parse (f v) rest)
+
+
+instance MonadPlus Parser where
+ mzero = P (\inp => Left "Parse Error")
+ mplus p q = P (\inp => case parse p inp of
+ Left msg => parse q inp
Right (v,out) => Right(v,out))
-
-{-
-Basic parsers
--------------
--}
-
-failure : String -> Parser a
-failure msg = P (\inp => Left msg)
-
-item : Parser Char
-item = P (\inp => case unpack inp of
- [] => Left "Error! Parsing empty list."
+
+{-
+Basic parsers
+-------------
+-}
+
+failure : String -> Parser a
+failure msg = P (\inp => Left msg)
+
+item : Parser Char
+item = P (\inp => case unpack inp of
+ [] => Left "Error! Parsing empty list."
(x::xs) => Right (x, pack xs))
-
+
{-
-Choice
---------
----}
-
-(|||) : Parser a -> Parser a -> Parser a
-p ||| q = p `mplus` q
-
-
---{-
---Derived primitives
----}
-
-sat : (Char -> Bool) -> Parser Char
+Choice
+--------
+---}
+
+(|||) : Parser a -> Parser a -> Parser a
+p ||| q = p `mplus` q
+
+
+--{-
+--Derived primitives
+---}
+
+sat : (Char -> Bool) -> Parser Char
sat p = item >>= (\x => if p x then return x else failure "failed")
-
-oneof : List Char -> Parser Char
-oneof xs = sat (\x => elem x xs)
-
-digit : Parser Char
-digit = sat isDigit
-
-lower : Parser Char
-lower = sat isLower
-
-upper : Parser Char
-upper = sat isUpper
-
-letter : Parser Char
-letter = sat isAlpha
-
-alphanum : Parser Char
-alphanum = sat isAlphaNum
-
-char : Char -> Parser Char
-char x = sat (== x)
-
-string : String -> Parser String
-helper : List Char -> Parser (List Char)
-string s = do result <- helper (unpack s)
- return (pack result)
-
-helper [] = return []
-helper (x::xs) = do char x
- string (cast xs)
- return (x :: xs)
-
-many1 : Parser a -> Parser (List a)
-many : Parser a -> Parser (List a)
-many1 p = do v <- p
- vs <- many p
- return (v::vs)
-
-
-many p = many1 p `mplus` return []
-
-
-
-ident : Parser String
-ident = do x <- letter
- xs <- many1 alphanum
- return (pack(x::xs))
-
-
-nat : Parser Int
-nat = do xs <- many digit
- return (cast (cast xs))
-
-
-int : Parser Int
-int = do char '-'
- n <- nat
- return (-n)
- `mplus` nat
-
-space : Parser ()
-space = do many (sat isSpace)
- return ()
---{-
---Ignoring spacing
----}
-
-token : Parser a -> Parser a
-token p = do space
- v <- p
- space
- return v
-
-identifier : Parser String
-identifier = token ident
-
-natural : Parser Int
-natural = token nat
-
-integer : Parser Int
-integer = token int
-
-symbol : String -> Parser String
-symbol xs = token (string xs)
+
+oneof : List Char -> Parser Char
+oneof xs = sat (\x => elem x xs)
+
+digit : Parser Char
+digit = sat isDigit
+
+lower : Parser Char
+lower = sat isLower
+
+upper : Parser Char
+upper = sat isUpper
+
+letter : Parser Char
+letter = sat isAlpha
+
+alphanum : Parser Char
+alphanum = sat isAlphaNum
+
+char : Char -> Parser Char
+char x = sat (== x)
+
+string : String -> Parser String
+helper : List Char -> Parser (List Char)
+string s = do result <- helper (unpack s)
+ return (pack result)
+
+helper [] = return []
+helper (x::xs) = do char x
+ string (cast xs)
+ return (x :: xs)
+
+many1 : Parser a -> Parser (List a)
+many : Parser a -> Parser (List a)
+many1 p = do v <- p
+ vs <- many p
+ return (v::vs)
+
+
+many p = many1 p `mplus` return []
+
+
+
+ident : Parser String
+ident = do x <- letter
+ xs <- many1 alphanum
+ return (pack(x::xs))
+
+
+nat : Parser Int
+nat = do xs <- many digit
+ return (cast (cast xs))
+
+
+int : Parser Int
+int = do char '-'
+ n <- nat
+ return (-n)
+ `mplus` nat
+
+space : Parser ()
+space = do many (sat isSpace)
+ return ()
+--{-
+--Ignoring spacing
+---}
+
+token : Parser a -> Parser a
+token p = do space
+ v <- p
+ space
+ return v
+
+identifier : Parser String
+identifier = token ident
+
+natural : Parser Int
+natural = token nat
+
+integer : Parser Int
+integer = token int
+
+symbol : String -> Parser String
+symbol xs = token (string xs)
--apply : Parser a -> String -> List (a,String)
--apply p = parse (space >>= (\_ => p))
--{-
--- Expressions
+-- Expressions
---}
factor : Parser Int
View
@@ -89,7 +89,7 @@ Executable idris
Paths_idris
Build-depends: base>=4 && <5, parsec, mtl, Cabal,
- haskeline>=0.7, split,
+ haskeline>=0.7, split, directory,
containers, process, transformers, filepath,
directory, binary, bytestring, pretty
View
@@ -289,11 +289,19 @@ fwrite (FHandle h) s = do_fwrite h s
partial
do_feof : Ptr -> IO Int
-do_feof h = mkForeign (FFun "feof" [FPtr] FInt) h
+do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
feof : File -> IO Bool
feof (FHandle h) = do eof <- do_feof h
- return (not (eof == 0))
+ return (not (eof == 0))
+
+partial
+do_ferror : Ptr -> IO Int
+do_ferror h = mkForeign (FFun "fileError" [FPtr] FInt) h
+
+ferror : File -> IO Bool
+ferror (FHandle h) = do err <- do_ferror h
+ return (not (err == 0))
partial
nullPtr : Ptr -> IO Bool
Oops, something went wrong.

0 comments on commit fd5cddb

Please sign in to comment.