git.iko.soy/Idris-dev
on master help sign in
More string and char primitives
d9834c1Edwin Brady
lib/builtins.idr+20
compare with master
unifiedsplit
@@ -107,6 +107,14 @@ instance Eq Float where {
107 (==) = boolOp prim__eqFloat;
107 (==) = boolOp prim__eqFloat;
108}
108}
109
109
110+instance Eq Char where {
111+ (==) = boolOp prim__eqChar;
112+}
113+
114+instance Eq String where {
115+ (==) = boolOp prim__eqString;
116+}
117+
110data Ordering = LT | EQ | GT;
118data Ordering = LT | EQ | GT;
111
119
112class Eq a => Ord a where {
120class Eq a => Ord a where {
@@ -150,6 +158,18 @@ instance Ord Float where {
150 GT;
158 GT;
151}
159}
152
160
161+instance Ord Char where {
162+ compare x y = if (x == y) then EQ else
163+ if (boolOp prim__ltChar x y) then LT else
164+ GT;
165+}
166+
167+instance Ord String where {
168+ compare x y = if (x == y) then EQ else
169+ if (boolOp prim__ltString x y) then LT else
170+ GT;
171+}
172+
153class Eq a => Num a where {
173class Eq a => Num a where {
154 (+) : a -> a -> a;
174 (+) : a -> a -> a;
155 (-) : a -> a -> a;
175 (-) : a -> a -> a;
lib/prelude.idr+1−1
@@ -136,7 +136,7 @@ putStrLn : String -> IO ();
136putStrLn x = putStr (x ++ "\n");
136putStrLn x = putStr (x ++ "\n");
137
137
138print : Show a => a -> IO ();
138print : Show a => a -> IO ();
139−print = putStrLn . show;
139+print x = putStrLn (show x);
140
140
141readLine : IO String;
141readLine : IO String;
142readLine = mkForeign (FFun "readStr" Nil FString);
142readLine = mkForeign (FFun "readStr" Nil FString);
src/Idris/Primitives.hs+25
@@ -53,6 +53,8 @@ strHead x = foreign_ tyChar "strHead" [(x, tyString)]
53strTail x = foreign_ tyString "strTail" [(x, tyString)]
53strTail x = foreign_ tyString "strTail" [(x, tyString)]
54strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]
54strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]
55strRev x = foreign_ tyString "strrev" [(x, tyString)]
55strRev x = foreign_ tyString "strrev" [(x, tyString)]
56+strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
57+strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
56
58
57primitives =
59primitives =
58 -- operators
60 -- operators
@@ -74,6 +76,16 @@ primitives =
74 (eOp E.gt_),
76 (eOp E.gt_),
75 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
77 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
76 (eOp E.gte_),
78 (eOp E.gte_),
79+ Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
80+ (eOp E.eq_),
81+ Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
82+ (eOp E.lt_),
83+ Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
84+ (eOp E.lte_),
85+ Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
86+ (eOp E.gt_),
87+ Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
88+ (eOp E.gte_),
77 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
89 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
78 (eOpFn tyBigInt tyBigInt "addBig"),
90 (eOpFn tyBigInt tyBigInt "addBig"),
79 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
91 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
@@ -112,6 +124,10 @@ primitives =
112 (eOp E.gteF_),
124 (eOp E.gteF_),
113 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
125 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
114 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
126 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
127+ Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
128+ ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")),
129+ Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
130+ ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")),
115 -- Conversions
131 -- Conversions
116 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
132 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
117 ([E.name "x"], strToInt (fun "x")),
133 ([E.name "x"], strToInt (fun "x")),
@@ -166,6 +182,15 @@ bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0
166 Just $ VConstant (I i)
182 Just $ VConstant (I i)
167bfBin _ _ = Nothing
183bfBin _ _ = Nothing
168
184
185+bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
186+ Just $ VConstant (I i)
187+bcBin _ _ = Nothing
188+
189+bsBin op [VConstant (Str x), VConstant (Str y)]
190+ = let i = (if op x y then 1 else 0) in
191+ Just $ VConstant (I i)
192+bsBin _ _ = Nothing
193+
169sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
194sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
170sBin _ _ = Nothing
195sBin _ _ = Nothing
171
196
tutorial/intro.tex+2−2
@@ -39,8 +39,8 @@ app : Vect a n -> Vect a m -> Vect a (n + m);
39\useverb{appendv}
39\useverb{appendv}
40
40
41
41
42−This tutorial introduces \Idris{}, a general purpose dependently typed functional
42+This tutorial introduces \Idris{}, a general purpose functional
43−programming language.
43+programming language with dependent types.
44The goal of the \Idris{} project is to build a dependently typed language suitable
44The goal of the \Idris{} project is to build a dependently typed language suitable
45for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
45for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
46which aims to generate efficient executable code. It also has a lightweight foreign
46which aims to generate efficient executable code. It also has a lightweight foreign