20bf4d7 · Idris-dev · git.iko.soy

interp.idr−1

compare with master

unifiedsplit

@@ -1,4 +1,3 @@

1−import nat;

2

1

3data Ty = TyNat | TyFun Ty Ty;

2data Ty = TyNat | TyFun Ty Ty;

4

3

nat.idr → lib/nat.idrrenamed

The content is the same.

lib/prelude.idrnew file+71

@@ -0,0 +1,71 @@

1+import nat;

2+

3+data Bool = False | True;

4+

5+infixl 5 ==, /=, ==.;

6+infixl 6 <, <=, >, >=, <., <=., >., >=.;

7+infixl 7 <<, >>;

8+infixl 8 +,-,++,+.,-.;

9+infixl 9 *,/,*.,/.;

10+

11+intToBool : Int -> Bool;

12+intToBool 0 = False;

13+intToBool x = True;

14+

15+boolOp : (a -> a -> Int) -> a -> a -> Bool;

16+boolOp op x y = intToBool (op x y);

17+

18+(+) : Int -> Int -> Int;

19+(+) = prim__addInt;

20+

21+(-) : Int -> Int -> Int;

22+(-) = prim__subInt;

23+

24+(*) : Int -> Int -> Int;

25+(*) = prim__mulInt;

26+

27+div : Int -> Int -> Int;

28+div = prim__divInt;

29+

30+(==) : Int -> Int -> Bool;

31+(==) = boolOp prim__eqInt;

32+

33+(<) : Int -> Int -> Bool;

34+(<) = boolOp prim__ltInt;

35+

36+(<=) : Int -> Int -> Bool;

37+(<=) = boolOp prim__lteInt;

38+

39+(>) : Int -> Int -> Bool;

40+(>) = boolOp prim__gtInt;

41+

42+(>=) : Int -> Int -> Bool;

43+(>=) = boolOp prim__gteInt;

44+

45+(+.) : Float -> Float -> Float;

46+(+.) = prim__addFloat;

47+

48+(-.) : Float -> Float -> Float;

49+(-.) = prim__subFloat;

50+

51+(*.) : Float -> Float -> Float;

52+(*.) = prim__mulFloat;

53+

54+(/.) : Float -> Float -> Float;

55+(/.) = prim__divFloat;

56+

57+(==.) : Float -> Float -> Bool;

58+(==.) = boolOp prim__eqFloat;

59+

60+(<.) : Float -> Float -> Bool;

61+(<.) = boolOp prim__ltFloat;

62+

63+(<=.) : Float -> Float -> Bool;

64+(<=.) = boolOp prim__lteFloat;

65+

66+(>.) : Float -> Float -> Bool;

67+(>.) = boolOp prim__gtFloat;

68+

69+(>=.) : Float -> Float -> Bool;

70+(>=.) = boolOp prim__gteFloat;

71+

miniidris.cabal+3

@@ -14,6 +14,9 @@ Description: An experimental new version of Idris

14Cabal-Version: >= 1.6

15Build-type: Simple

16

17+Data-files: *.idr

18+Data-dir: lib

19+

17Executable miniidris

20Executable miniidris

18 Main-is: Main.hs

21 Main-is: Main.hs

19 hs-source-dirs: src

22 hs-source-dirs: src

prims.mi+2

@@ -1,3 +1,5 @@

1+import nat;

2+

1data Bool = False | True;

3data Bool = False | True;

2

4

3infixl 5 ==, /=, ==.;

5infixl 5 ==, /=, ==.;

src/Main.hs+8−3

@@ -27,6 +27,8 @@ import Idris.Imports

27

28data Opt = Filename String

29 | Version

30+ | NoPrelude

31+ | NoREPL

30 | OLogging Int

32 | OLogging Int

31 deriving Eq

33 deriving Eq

32

34

@@ -39,8 +41,9 @@ runIdris opts =

39 do let inputs = opt getFile opts

41 do let inputs = opt getFile opts

40 mapM_ makeOption opts

42 mapM_ makeOption opts

41 elabPrims

43 elabPrims

44+ when (not (NoPrelude `elem` opts)) $ loadModule "prelude"

42 mapM_ loadModule inputs

45 mapM_ loadModule inputs

43− repl

46+ when (not (NoREPL `elem` opts)) $ repl

44 where

47 where

45 makeOption (OLogging i) = setLogLevel i

48 makeOption (OLogging i) = setLogLevel i

46 makeOption _ = return ()

49 makeOption _ = return ()

@@ -57,8 +60,10 @@ usage = do putStrLn "You're doing it wrong"

57

60

58parseArgs :: [String] -> IO [Opt]

61parseArgs :: [String] -> IO [Opt]

59parseArgs [] = return []

62parseArgs [] = return []

60−parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

63+parseArgs ("--log":lvl:ns) = liftM (OLogging (read lvl) : ) (parseArgs ns)

64+parseArgs ("--noprelude":ns) = liftM (NoPrelude : ) (parseArgs ns)

65+parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

61−parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

66+parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

62

67

63{-

68{-

64main'

69main'