Skip to content
Browse files

Added lib/ and prelude

  • Loading branch information...
1 parent b1419b2 commit 20bf4d7d2e726ae9b4800f50bfe2a7e5a8cc90ef Edwin Brady committed Oct 14, 2011
Showing with 84 additions and 4 deletions.
  1. +0 −1 interp.idr
  2. 0 { → lib}/nat.idr
  3. +71 −0 lib/prelude.idr
  4. +3 −0 miniidris.cabal
  5. +2 −0 prims.mi
  6. +8 −3 src/Main.hs
View
1 interp.idr
@@ -1,4 +1,3 @@
-import nat;
data Ty = TyNat | TyFun Ty Ty;
View
0 nat.idr → lib/nat.idr
File renamed without changes.
View
71 lib/prelude.idr
@@ -0,0 +1,71 @@
+import nat;
+
+data Bool = False | True;
+
+infixl 5 ==, /=, ==.;
+infixl 6 <, <=, >, >=, <., <=., >., >=.;
+infixl 7 <<, >>;
+infixl 8 +,-,++,+.,-.;
+infixl 9 *,/,*.,/.;
+
+intToBool : Int -> Bool;
+intToBool 0 = False;
+intToBool x = True;
+
+boolOp : (a -> a -> Int) -> a -> a -> Bool;
+boolOp op x y = intToBool (op x y);
+
+(+) : Int -> Int -> Int;
+(+) = prim__addInt;
+
+(-) : Int -> Int -> Int;
+(-) = prim__subInt;
+
+(*) : Int -> Int -> Int;
+(*) = prim__mulInt;
+
+div : Int -> Int -> Int;
+div = prim__divInt;
+
+(==) : Int -> Int -> Bool;
+(==) = boolOp prim__eqInt;
+
+(<) : Int -> Int -> Bool;
+(<) = boolOp prim__ltInt;
+
+(<=) : Int -> Int -> Bool;
+(<=) = boolOp prim__lteInt;
+
+(>) : Int -> Int -> Bool;
+(>) = boolOp prim__gtInt;
+
+(>=) : Int -> Int -> Bool;
+(>=) = boolOp prim__gteInt;
+
+(+.) : Float -> Float -> Float;
+(+.) = prim__addFloat;
+
+(-.) : Float -> Float -> Float;
+(-.) = prim__subFloat;
+
+(*.) : Float -> Float -> Float;
+(*.) = prim__mulFloat;
+
+(/.) : Float -> Float -> Float;
+(/.) = prim__divFloat;
+
+(==.) : Float -> Float -> Bool;
+(==.) = boolOp prim__eqFloat;
+
+(<.) : Float -> Float -> Bool;
+(<.) = boolOp prim__ltFloat;
+
+(<=.) : Float -> Float -> Bool;
+(<=.) = boolOp prim__lteFloat;
+
+(>.) : Float -> Float -> Bool;
+(>.) = boolOp prim__gtFloat;
+
+(>=.) : Float -> Float -> Bool;
+(>=.) = boolOp prim__gteFloat;
+
View
3 miniidris.cabal
@@ -14,6 +14,9 @@ Description: An experimental new version of Idris
Cabal-Version: >= 1.6
Build-type: Simple
+Data-files: *.idr
+Data-dir: lib
+
Executable miniidris
Main-is: Main.hs
hs-source-dirs: src
View
2 prims.mi
@@ -1,3 +1,5 @@
+import nat;
+
data Bool = False | True;
infixl 5 ==, /=, ==.;
View
11 src/Main.hs
@@ -27,6 +27,8 @@ import Idris.Imports
data Opt = Filename String
| Version
+ | NoPrelude
+ | NoREPL
| OLogging Int
deriving Eq
@@ -39,8 +41,9 @@ runIdris opts =
do let inputs = opt getFile opts
mapM_ makeOption opts
elabPrims
+ when (not (NoPrelude `elem` opts)) $ loadModule "prelude"
mapM_ loadModule inputs
- repl
+ when (not (NoREPL `elem` opts)) $ repl
where
makeOption (OLogging i) = setLogLevel i
makeOption _ = return ()
@@ -57,8 +60,10 @@ usage = do putStrLn "You're doing it wrong"
parseArgs :: [String] -> IO [Opt]
parseArgs [] = return []
-parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
-parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
+parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)
+parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)
+parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)
+parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)
{-
main'

0 comments on commit 20bf4d7

Please sign in to comment.
Something went wrong with that request. Please try again.