git.iko.soy/Idris-dev
on master help sign in
Added some library files
commit38a6bc7695135477e91420f5f6cdc287503856ba authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 14 Oct 2011, 21:45 (15 years ago) parent9d1ecc8
4 files changed+68−1
compare with master
unifiedsplit
lib/io.idr+39 lib/list.idr+9 lib/prelude.idr+15 src/Idris/Primitives.hs+5−1
lib/io.idrnew file+39
@@ -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+
11+data FTy = FInt | FFloat | FChar | FString | FPtr | FUnit;
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 <<, >>;
1010infixl 8 +,-,++,+.,-.;
1111infixl 9 *,/,*.,/.;
1212
13+--- Numeric operators
14+
1315intToBool : Int -> Bool;
1416intToBool 0 = False;
1517intToBool x = True;
@@ -71,3 +73,16 @@ div = prim__divInt;
7173(>=.) : Float -> Float -> Bool;
7274(>=.) = boolOp prim__gteFloat;
7375
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 =
3333 Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<)),
3434 Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=)),
3535 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 (++))
3738 ]
3839
3940iBin 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
4849 Just $ VConstant (I i)
4950bfBin _ _ = Nothing
5051
52+sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
53+sBin _ _ = Nothing
54+
5155elabPrim :: Prim -> Idris ()
5256elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)
5357