38a6bc7 · Idris-dev · git.iko.soy

lib/io.idrnew file+39

compare with master

unifiedsplit

@@ -0,0 +1,39 @@

1+import list;

2+

3+data IO a = prim__IO a;

4+

5+io_bind : IO a -> (a -> IO b) -> IO b;

6+io_bind (prim__IO v) k = k v;

7+

8+io_return : a -> IO a;

9+io_return = prim__IO;

10+

12+

13+interpFTy : FTy -> Set;

14+interpFTy FInt = Int;

15+interpFTy FFloat = Float;

16+interpFTy FChar = Char;

17+interpFTy FString = String;

18+interpFTy FPtr = Ptr;

19+interpFTy FUnit = ();

20+

21+ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;

22+ForeignTy xs t = mkForeign (rev xs) (IO (interpFTy t)) where {

23+ mkForeign : List FTy -> Set -> Set;

24+ mkForeign Nil ty = ty;

25+ mkForeign (Cons s ss) ty = mkForeign ss (interpFTy s -> ty);

26+}

27+

28+data FEnv : List FTy -> Set where

29+ FEmpty : FEnv Nil

30+ | FCons : {xs:List FTy} ->

31+ interpFTy x -> FEnv xs -> FEnv (Cons x xs);

32+

33+data Foreign : Set -> Set where

34+ FFun : String -> (xs:List FTy) -> (t:FTy) ->

35+ Foreign (ForeignTy xs t);

36+

37+mkForeign : Foreign x -> x;

38+-- mkForeign compiled as primitive

39+

lib/list.idrnew file+9

@@ -0,0 +1,9 @@

1+data List a = Nil | Cons a (List a);

2+

3+rev : List a -> List a;

4+rev xs = revAcc Nil xs

5+ where {

6+ revAcc : List a -> List a -> List a;

7+ revAcc acc Nil = acc;

8+ revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;

9+ }

lib/prelude.idr+15

@@ -10,6 +10,8 @@ infixl 7 <<, >>;

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

11infixl 9 *,/,*.,/.;

12

13+--- Numeric operators

14+

13intToBool : Int -> Bool;

15intToBool : Int -> Bool;

14intToBool 0 = False;

16intToBool 0 = False;

15intToBool x = True;

17intToBool x = True;

@@ -71,3 +73,16 @@ div = prim__divInt;

71(>=.) : Float -> Float -> Bool;

73(>=.) : Float -> Float -> Bool;

72(>=.) = boolOp prim__gteFloat;

74(>=.) = boolOp prim__gteFloat;

73

75

76+--- string operators

77+

78+(++) : String -> String -> String;

79+(++) = prim__concat;

80+

81+---- some basic io

82+

83+putStr : String -> IO ();

84+putStr = mkForeign (FFun "putStr" (Cons FString Nil) FUnit);

85+

86+putStrLn : String -> IO ();

87+putStrLn x = putStr (x ++ "\n");

88+

src/Idris/Primitives.hs+5−1

@@ -33,7 +33,8 @@ primitives =

33 Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<)),

34 Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=)),

35 Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>)),

36− Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))

36+ Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=)),

37+ Prim (UN ["prim__concat"]) (ty [StrType, StrType] StrType) 2 (sBin (++))

37 ]

38 ]

38

39

39iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

40iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

@@ -48,6 +49,9 @@ bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0

48 Just $ VConstant (I i)

49 Just $ VConstant (I i)

49bfBin _ _ = Nothing

50bfBin _ _ = Nothing

50

51

52+sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

53+sBin _ _ = Nothing

54+

51elabPrim :: Prim -> Idris ()

55elabPrim :: Prim -> Idris ()

52elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)

56elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)

53

57